walther@60318: (* Knowledge/poly.sml neuper@37906: author: Matthias Goldgruber 2003 neuper@37906: (c) due to copyright terms neuper@37906: neuper@42395: LEGEND: neuper@42395: WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml' neuper@42395: examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml' neuper@38022: *) neuper@42395: walther@60318: "-----------------------------------------------------------------------------------------------"; walther@60318: "-----------------------------------------------------------------------------------------------"; walther@60318: "table of contents -----------------------------------------------------------------------------"; walther@60318: "-----------------------------------------------------------------------------------------------"; walther@60318: "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; walther@60318: "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; walther@60318: "-------- fun is_polyexp -----------------------------------------------------------------------"; walther@60318: "-------- fun has_degree_in --------------------------------------------------------------------"; walther@60318: "-------- fun mono_deg_in ----------------------------------------------------------------------"; walther@60318: "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------"; walther@60318: "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------"; walther@60318: "-------- investigate (new 2002) uniary minus --------------------------------------------------"; walther@60318: "-------- fun sort_variables -------------------------------------------------------------------"; walther@60318: "-------- rebuild fun is_addUnordered (1 + 2 * x \ 4 + - 4 * x \ 4 + x \ 8) ---------------------"; walther@60318: "-------- fun is_addUnordered (x \ 2 * y \ 2 + x \ 3 * y) --------------------------------------"; walther@60318: "-------- check make_polynomial with simple terms ----------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x \ 2 * x) -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x - a) \ 3 -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; walther@60318: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; walther@60318: "-------- examples from textbook Schalk I ------------------------------------------------------"; walther@60318: "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------"; walther@60318: "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------"; walther@60318: "-------- check pbl 'polynomial simplification' -----------------------------------------------"; walther@60318: "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------"; walther@60318: "-------- interSteps for Schalk 299a -----------------------------------------------------------"; walther@60318: "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------"; walther@60318: "-------- ord_make_polynomial ------------------------------------------------------------------"; walther@60318: "-----------------------------------------------------------------------------------------------"; walther@60318: "-----------------------------------------------------------------------------------------------"; walther@60318: "-----------------------------------------------------------------------------------------------"; neuper@37906: neuper@37906: walther@60318: "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; walther@60318: "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; walther@60318: "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; walther@60318: (* indentation indicates call hierarchy: walther@60318: "~~~~~ fun is_addUnordered walther@60318: "~~~~~~~ fun is_polyexp walther@60318: "~~~~~~~ fun sort_monoms walther@60318: "~~~~~~~~~ fun sort_monList walther@60318: "~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order walther@60318: "~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order walther@60318: "~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order walther@60318: "~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order walther@60318: "~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv walther@60318: "~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv walther@60318: "~~~~~~~~~~~~~~~ fun monom_degree : term list -> int walther@60318: "~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order walther@60318: "~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option walther@60318: "~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string walther@60318: "~~~~~ fun is_multUnordered walther@60318: "~~~~~~~ fun sort_variables walther@60318: "~~~~~~~~~ fun sort_varList walther@60318: "~~~~~~~~~~~ fun var_ord walther@60318: "~~~~~~~~~~~~~ fun get_basStr used twice --^^ walther@60318: "~~~~~~~~~~~~~ fun get_potStr used twice --^^ wneuper@59529: walther@60318: fun int_ord (i1, i2) = walther@60318: (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)}; walther@60318: Int.compare (i1, i2) walther@60318: ); walther@60318: fun var_ord (a, b) = walther@60318: (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", walther@60318: sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; walther@60318: prod_ord string_ord string_ord walther@60318: ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) walther@60318: ); walther@60318: fun var_ord_revPow (a, b: term) = walther@60318: (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", walther@60318: sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; walther@60318: prod_ord string_ord string_ord_rev walther@60318: ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) walther@60318: ); walther@60318: fun sort_varList ts = walther@60318: (@{print} {a = "sort_varList", args = UnparseC.terms ts}; walther@60318: sort var_ord ts walther@60318: ); walther@60318: fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL) walther@60318: | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS) walther@60318: | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER) walther@60318: | dict_cond_ord elem_ord cond (x :: xs, y :: ys) = walther@60318: (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")", walther@60318: is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"}; walther@60318: case (cond x, cond y) of walther@60318: (false, false) => walther@60318: (case elem_ord (x, y) of walther@60318: EQUAL => dict_cond_ord elem_ord cond (xs, ys) walther@60318: | ord => ord) walther@60318: | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys) walther@60318: | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys) walther@60318: | (true, true) => dict_cond_ord elem_ord cond (xs, ys) walther@60318: ); walther@60318: fun compare_koeff_ord (xs, ys) = walther@60318: (@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")", walther@60318: sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"}; walther@60318: string_ord walther@60318: ((koeff2ordStr o get_koeff_of_mon) xs, walther@60318: (koeff2ordStr o get_koeff_of_mon) ys) walther@60318: ); walther@60318: fun var_ord (a,b: term) = walther@60318: (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", walther@60318: sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; walther@60318: prod_ord string_ord string_ord walther@60318: ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) walther@60318: ); walther@60318: *) walther@60318: walther@60318: walther@60318: "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; walther@60318: "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; walther@60318: "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; walther@60318: (* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls. walther@60318: walther@60318: sym_real_mult_minus1 = "- ?z = - 1 * ?z" *) walther@60318: @{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *) walther@60318: val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *) walther@60318: val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real"; walther@60318: walther@60318: val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac; walther@60318: if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*)) walther@60318: else error "thm - ?z = - 1 * ?z loops with new numerals"; walther@60318: walther@60318: walther@60318: "-------- fun is_polyexp -----------------------------------------------------------------------"; walther@60318: "-------- fun is_polyexp -----------------------------------------------------------------------"; walther@60318: "-------- fun is_polyexp -----------------------------------------------------------------------"; walther@60318: val t = TermC.str2term "x / x"; wneuper@59529: if is_polyexp t then error "NOT is_polyexp (x / x)" else (); wneuper@59529: walther@60318: val t = TermC.str2term "-1 * A * 3"; wneuper@59529: if is_polyexp t then () else error "is_polyexp (-1 * A * 3)"; wneuper@59529: walther@60318: val t = TermC.str2term "-1 * AA * 3"; wneuper@59529: if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)"; neuper@38022: walther@60318: val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real"; walther@60318: if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))"; walther@60318: walther@60318: "-------- fun has_degree_in --------------------------------------------------------------------"; walther@60318: "-------- fun has_degree_in --------------------------------------------------------------------"; walther@60318: "-------- fun has_degree_in --------------------------------------------------------------------"; walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "1"; wneuper@59522: if has_degree_in t v = 0 then () else error "has_degree_in (1) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "1"; wneuper@59522: if has_degree_in t v = 0 then () else error "has_degree_in (1) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; wneuper@59522: if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c"; wneuper@59522: if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c"; wneuper@59522: if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c"; wneuper@59522: if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \ 7"; walther@60242: if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \ 7) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \ 7"; walther@60242: if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \ 7) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "x \ 7"; walther@60242: if has_degree_in t v = 7 then () else error "has_degree_in (x \ 7) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "AA \ 7"; walther@60242: if has_degree_in t v = 7 then () else error "has_degree_in (AA \ 7) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x"; wneuper@59522: if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA"; wneuper@59522: if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "x"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in (x) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "AA"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA"; wneuper@59522: wneuper@59522: (*----------*) walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x"; wneuper@59522: walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA"; wneuper@59522: if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA"; wneuper@59522: walther@60318: "-------- fun mono_deg_in ----------------------------------------------------------------------"; walther@60318: "-------- fun mono_deg_in ----------------------------------------------------------------------"; walther@60318: "-------- fun mono_deg_in ----------------------------------------------------------------------"; walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "x"; wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \ 7"; walther@60242: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \ 7) x changed"; wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "x \ 7"; walther@60242: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \ 7) x changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x"; wneuper@59522: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x"; wneuper@59522: if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "x"; wneuper@59522: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)"; wneuper@59522: if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x"; wneuper@59522: if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed"; wneuper@59522: wneuper@59522: (*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *) wneuper@59522: val thy = @{theory Partial_Fractions} walther@60230: val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \ 7"; walther@60242: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \ 7) AA changed"; wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "AA \ 7"; walther@60242: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \ 7) AA changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA"; wneuper@59522: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA"; wneuper@59522: if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "AA"; wneuper@59522: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)"; wneuper@59522: if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed"; wneuper@59522: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA"; wneuper@59522: if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed"; wneuper@59522: walther@60318: "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------"; walther@60318: "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------"; walther@60318: "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------"; wneuper@59522: val thy = @{theory Partial_Fractions} walther@60242: val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \ 2) has_degree_in x) = 2"; wneuper@59522: val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr; wneuper@59522: walther@60242: val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \ 2) has_degree_in AA) = 2"; wneuper@59522: val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr; wneuper@59522: walther@60318: "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------"; walther@60318: "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------"; walther@60318: "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \ 2) is_expanded_in x"; wneuper@59522: val SOME (id, t') = eval_is_expanded_in 0 0 t 0; walther@60317: if UnparseC.term t' = "- 8 - 2 * x + x \ 2 is_expanded_in x = True" walther@60317: andalso id = "- 8 - 2 * x + x \ 2 is_expanded_in x = True" wneuper@59522: then () else error "eval_is_expanded_in x ..changed"; wneuper@59522: wneuper@59522: val thy = @{theory Partial_Fractions} walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \ 2) is_expanded_in AA"; wneuper@59522: val SOME (id, t') = eval_is_expanded_in 0 0 t 0; walther@60317: if UnparseC.term t' = "- 8 - 2 * AA + AA \ 2 is_expanded_in AA = True" walther@60317: andalso id = "- 8 - 2 * AA + AA \ 2 is_expanded_in AA = True" wneuper@59522: then () else error "eval_is_expanded_in AA ..changed"; wneuper@59522: wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \ 2) is_poly_in x"; wneuper@59522: val SOME (id, t') = eval_is_poly_in 0 0 t 0; walther@60242: if UnparseC.term t' = "8 + 2 * x + x \ 2 is_poly_in x = True" walther@60242: andalso id = "8 + 2 * x + x \ 2 is_poly_in x = True" wneuper@59522: then () else error "is_poly_in x ..changed"; wneuper@59522: walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \ 2) is_poly_in AA"; wneuper@59522: val SOME (id, t') = eval_is_poly_in 0 0 t 0; walther@60242: if UnparseC.term t' = "8 + 2 * AA + AA \ 2 is_poly_in AA = True" walther@60242: andalso id = "8 + 2 * AA + AA \ 2 is_poly_in AA = True" wneuper@59522: then () else error "is_poly_in AA ..changed"; wneuper@59522: wneuper@59522: wneuper@59522: val thy = @{theory Partial_Fractions} walther@60242: val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \ 2) has_degree_in x) = 2"; wneuper@59522: val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr; wneuper@59522: walther@60242: val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \ 2) has_degree_in AA) = 2"; wneuper@59522: val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr; wneuper@59522: walther@60318: "-------- investigate (new 2002) uniary minus --------------------------------------------------"; walther@60318: "-------- investigate (new 2002) uniary minus --------------------------------------------------"; walther@60318: "-------- investigate (new 2002) uniary minus --------------------------------------------------"; wenzelm@60203: val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*) walther@60230: TermC.atomty t; wneuper@59117: (* wneuper@59117: *** Const (HOL.Trueprop, bool => prop) wneuper@59117: *** . Const (HOL.eq, real => real => bool) wneuper@59117: *** . . Const (Groups.minus_class.minus, real => real => real) wneuper@59117: *** . . . Const (Groups.zero_class.zero, real) neuper@37906: *** . . . Var ((x, 0), real) wneuper@59117: *** . . Const (Groups.uminus_class.uminus, real => real) wneuper@59117: *** . . . Var ((x, 0), real) wneuper@59117: *) neuper@42395: case t of neuper@42395: Const ("HOL.Trueprop", _) $ wneuper@59117: (Const ("HOL.eq", _) $ wneuper@59117: (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $ wneuper@59117: Var (("x", 0), _)) $ wneuper@59117: (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => () neuper@42395: | _ => error "internal representation of \"0 - ?x = - ?x\" changed"; neuper@37906: walther@60318: walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "- 1"; walther@60230: TermC.atomty t; wneuper@59117: (* wneuper@59117: *** wneuper@59117: *** Free (-1, real) wneuper@59117: *** wneuper@59117: *) neuper@42395: case t of walther@60318: Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => () neuper@42395: | _ => error "internal representation of \"- 1\" changed"; neuper@37906: neuper@42395: "======= these external values all have the same internal representation"; neuper@42395: (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*) neuper@42395: (*----------------------------------- vvvvv -------------------------------------------*) walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "-x"; walther@60230: TermC.atomty t; neuper@37906: (**** ------------- neuper@37906: *** Free ( -x, real)*) neuper@42395: case t of neuper@42395: Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () neuper@42395: | _ => error "internal representation of \"-x\" changed"; neuper@42395: (*----------------------------------- vvvvv -------------------------------------------*) walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "- x"; walther@60230: TermC.atomty t; neuper@37906: (**** ------------- neuper@37906: *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*) neuper@42395: case t of neuper@42395: Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () neuper@42395: | _ => error "internal representation of \"- x\" changed"; neuper@42395: (*----------------------------------- vvvvvv ------------------------------------------*) walther@60230: val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)"; walther@60230: TermC.atomty t; neuper@37906: (**** ------------- neuper@37906: *** Free ( -x, real)*) neuper@42395: case t of neuper@42395: Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () neuper@42395: | _ => error "internal representation of \"-(x)\" changed"; neuper@37906: walther@60318: walther@60318: "-------- fun sort_variables -------------------------------------------------------------------"; walther@60318: "-------- fun sort_variables -------------------------------------------------------------------"; walther@60318: "-------- fun sort_variables -------------------------------------------------------------------"; walther@60318: if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then () walther@60318: else error "lexicographic order CHANGED"; walther@60318: walther@60318: (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*) walther@60318: val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*) walther@60318: val t' = sort_variables t; walther@60318: if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then () walther@60318: else error "sort_variables 3 * b + a * 2 CHANGED"; walther@60318: walther@60318: "~~~~~~~ fun sort_variables , args:"; val (t) = (t); walther@60318: val ll = map monom2list (poly2list t); walther@60318: walther@60318: (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]"; walther@60318: (*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)], walther@60318: (*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)] walther@60318: (*+*) ] = map monom2list (poly2list t); walther@60318: walther@60318: val lls = map sort_varList ll; walther@60318: walther@60318: (*+*)case map sort_varList ll of walther@60318: (*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)], walther@60318: (*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)] walther@60318: (*+*) ] => () walther@60318: (*+*)| _ => error "map sort_varList CHANGED"; walther@60318: walther@60318: val T = type_of t; walther@60318: val ls = map (create_monom T) lls; walther@60318: walther@60318: (*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _), walther@60318: (*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls; walther@60318: walther@60318: (*+*)case map (create_monom T) lls of walther@60318: (*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _), walther@60318: (*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _) walther@60318: (*+*) ] => () walther@60318: (*+*)| _ => error "map (create_monom T) CHANGED"; walther@60318: walther@60318: val xxx = (*in*) create_polynom T ls (*end*); walther@60318: walther@60318: (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then () walther@60318: (*+*)else error "create_polynom CHANGED"; walther@60318: (* done by rewriting> 2 * a + 3 * b ? *) walther@60318: walther@60318: (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*) walther@60318: val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*) walther@60318: val t' = sort_variables t; walther@60318: if UnparseC.term t' = "3 * a + - 2 * a" then () walther@60318: else error "sort_variables 3 * a + - 2 * a CHANGED"; walther@60318: walther@60318: "~~~~~~~ fun sort_variables , args:"; val (t) = (t); walther@60318: val ll = map monom2list (poly2list t); walther@60318: walther@60318: (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)], walther@60318: (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*) walther@60318: (*+*) ] = map monom2list (poly2list t); walther@60318: walther@60318: val lls = map walther@60318: sort_varList ll; walther@60318: walther@60318: (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)], walther@60318: (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*) walther@60318: (*+*) ] = map sort_varList ll; walther@60318: walther@60318: map sort_varList ll; walther@60318: "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll); walther@60318: val sorted = sort var_ord ts; walther@60318: walther@60318: (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]" walther@60318: (*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED"; walther@60318: walther@60318: walther@60318: (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2" walther@60318: (*+*)then () else error "get_basStr - 2 CHANGED"; walther@60318: (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a" walther@60318: (*+*)then () else error "get_basStr a CHANGED"; walther@60318: walther@60318: walther@60318: "-------- rebuild fun is_addUnordered (1 + 2 * x \ 4 + - 4 * x \ 4 + x \ 8) ---------------------"; walther@60318: "-------- rebuild fun is_addUnordered (1 + 2 * x \ 4 + - 4 * x \ 4 + x \ 8) ---------------------"; walther@60318: "-------- rebuild fun is_addUnordered (1 + 2 * x \ 4 + - 4 * x \ 4 + x \ 8) ---------------------"; walther@60318: (* indentation partially indicates call hierarchy: walther@60318: "~~~~~ fun is_addUnordered walther@60318: "~~~~~~~ fun is_polyexp walther@60318: "~~~~~~~ fun sort_monoms walther@60318: "~~~~~~~~~ fun sort_monList walther@60318: "~~~~~~~~~~~ fun koeff_degree_ord walther@60318: "~~~~~~~~~~~~~ fun degree_ord walther@60318: "~~~~~~~~~~~~~~~ fun dict_cond_ord walther@60318: "~~~~~~~~~~~~~~~~~ fun var_ord_revPow walther@60318: "~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv walther@60318: "~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv walther@60318: "~~~~~~~~~~~~~~~ fun monom_degree walther@60318: "~~~~~~~~~~~~~ fun compare_koeff_ord walther@60318: "~~~~~~~~~~~~~~~ fun get_koeff_of_mon walther@60318: "~~~~~~~~~~~~~~~~~ fun koeff2ordStr walther@60318: "~~~~~ fun is_multUnordered walther@60318: "~~~~~~~ fun sort_variables walther@60318: "~~~~~~~~~ fun sort_varList walther@60318: "~~~~~~~~~~~ fun var_ord walther@60318: "~~~~~~~~~~~~~ fun get_basStr used twice --^^ walther@60318: "~~~~~~~~~~~~~ fun get_potStr used twice --^^ walther@60318: *) walther@60318: val t = TermC.str2term "(1 + 2 * x \ 4 + - 4 * x \ 4 + x \ 8) is_addUnordered"; walther@60318: walther@60318: eval_is_addUnordered "xxx" "yyy" t @{theory}; walther@60318: "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _, walther@60318: (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) = walther@60318: ("xxx", "yyy", t, @{theory}); walther@60318: walther@60318: (*if*) is_addUnordered arg; walther@60318: "~~~~~ fun is_addUnordered , args:"; val (t) = (arg); walther@60318: ((is_polyexp t) andalso not (t = sort_monoms t)); walther@60318: walther@60318: (t = sort_monoms t); walther@60318: "~~~~~~~ fun sort_monoms , args:"; val (t) = (t); walther@60318: val ll = map monom2list (poly2list t); walther@60318: val lls = walther@60318: walther@60318: sort_monList ll; walther@60318: "~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll); walther@60318: val xxx = walther@60318: walther@60318: sort koeff_degree_ord ll(*return value*); walther@60318: "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll); walther@60318: koeff_degree_ord: term list * term list -> order; walther@60318: (*we check all elements at once..*) walther@60318: val eee1 = ll |> nth 1; walther@60318: val eee2 = ll |> nth 2; walther@60318: val eee3 = ll |> nth 3; walther@60318: val eee3 = ll |> nth 3; walther@60318: val eee4 = ll |> nth 4; walther@60318: walther@60318: if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED"; walther@60318: if UnparseC.terms eee2 = "[\"2\", \"x \ 4\"]" then () else error "eee2 CHANGED"; walther@60318: if UnparseC.terms eee3 = "[\"- 4\", \"x \ 4\"]" then () else error "eee3 CHANGED"; walther@60318: if UnparseC.terms eee4 = "[\"x \ 8\"]" then () else error "eee4 CHANGED"; walther@60318: walther@60318: if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED"; walther@60318: if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED"; walther@60318: if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED"; walther@60318: if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED"; walther@60318: walther@60318: if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED"; walther@60318: if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED"; walther@60318: if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED"; walther@60318: if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED"; walther@60318: walther@60318: if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED"; walther@60318: if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED"; walther@60318: if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED"; walther@60318: if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED"; walther@60318: walther@60318: if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED"; walther@60318: if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED"; walther@60318: if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED"; walther@60318: if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED"; walther@60318: walther@60318: "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = (); walther@60318: degree_ord: term list * term list -> order; walther@60318: walther@60318: if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED"; walther@60318: if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED"; walther@60318: if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED"; walther@60318: if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED"; walther@60318: walther@60318: if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED"; walther@60318: if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED"; walther@60318: if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED"; walther@60318: if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED"; walther@60318: walther@60318: if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED"; walther@60318: if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED"; walther@60318: if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED"; walther@60318: if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED"; walther@60318: walther@60318: if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED"; walther@60318: if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED"; walther@60318: if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED"; walther@60318: if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED"; walther@60318: walther@60318: "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = (); walther@60318: dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order; walther@60318: dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order; walther@60318: dict_cond_ord var_ord_revPow is_nums: term list * term list -> order; walther@60318: val xxx = dict_cond_ord var_ord_revPow is_nums; walther@60318: (* output from: walther@60318: fun var_ord_revPow (a,b: term) = walther@60318: (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"}; walther@60318: @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; walther@60318: prod_ord string_ord string_ord_rev walther@60318: ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))); walther@60318: *) walther@60318: if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED"; walther@60318: if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED"; walther@60318: if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED"; walther@60318: if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED"; walther@60318: (*-------------------------------------------------------------------------------------*) walther@60318: if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED"; walther@60318: if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED"; walther@60318: if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED"; walther@60318: if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED"; walther@60318: (*-------------------------------------------------------------------------------------*) walther@60318: if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED"; walther@60318: if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED"; walther@60318: if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED"; walther@60318: if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED"; walther@60318: (*-------------------------------------------------------------------------------------*) walther@60318: if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED"; walther@60318: if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED"; walther@60318: if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED"; walther@60318: if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED"; walther@60318: (*-------------------------------------------------------------------------------------*) walther@60318: walther@60318: "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = (); walther@60318: (* we check all at once//*) walther@60318: if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED"; walther@60318: if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED"; walther@60318: if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED"; walther@60318: if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED"; walther@60318: walther@60318: "~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = (); walther@60318: compare_koeff_ord: term list * term list -> order; walther@60318: (* we check all at once//*) walther@60318: if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED"; walther@60318: if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED"; walther@60318: if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED"; walther@60318: if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED"; walther@60318: walther@60318: if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED"; walther@60318: if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED"; walther@60318: if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED"; walther@60318: if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED"; walther@60318: walther@60318: if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED"; walther@60318: if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED"; walther@60318: if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED"; walther@60318: if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED"; walther@60318: walther@60318: if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED"; walther@60318: if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED"; walther@60318: if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED"; walther@60318: if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED"; walther@60318: walther@60318: "~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = (); walther@60318: get_koeff_of_mon: term list -> term option; walther@60318: walther@60318: val SOME xxx1 = get_koeff_of_mon eee1; walther@60318: val SOME xxx2 = get_koeff_of_mon eee2; walther@60318: val SOME xxx3 = get_koeff_of_mon eee3; walther@60318: val NONE = get_koeff_of_mon eee4; walther@60318: walther@60318: if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED"; walther@60318: if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED"; walther@60318: if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED"; walther@60318: walther@60318: "~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = (); walther@60318: koeff2ordStr: term option -> string; walther@60318: if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED"; walther@60318: if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED"; walther@60318: if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED"; walther@60318: if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED"; walther@60318: walther@60318: walther@60318: "-------- fun is_addUnordered (x \ 2 * y \ 2 + x \ 3 * y) --------------------------------------"; walther@60318: "-------- fun is_addUnordered (x \ 2 * y \ 2 + x \ 3 * y) --------------------------------------"; walther@60318: "-------- fun is_addUnordered (x \ 2 * y \ 2 + x \ 3 * y) --------------------------------------"; walther@60318: val t = TermC.str2term "x \ 2 * y \ 2 + x * x \ 2 * y"; walther@60318: Rewrite.trace_on := false; walther@60318: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: UnparseC.term t = "x \ 2 * y \ 2 + x \ 3 * y"; walther@60318: if UnparseC.term t = "x \ 3 * y + x \ 2 * y \ 2" then () walther@60318: else error "poly.sml: diff.behav. in make_polynomial 23"; walther@60318: walther@60318: (** ) walther@60318: ## rls: order_add_rls_ on: x \ 2 * y \ 2 + x \ 3 * y walther@60318: ### rls: order_add_ on: x \ 2 * y \ 2 + x \ 3 * y walther@60318: ###### rls: Rule_Set.empty-is_addUnordered on: x \ 2 * y \ 2 + x \ 3 * y is_addUnordered walther@60318: ####### try calc: "Poly.is_addUnordered" walther@60318: ######## eval asms: "x \ 2 * y \ 2 + x \ 3 * y is_addUnordered = False" (*isa*) walther@60318: True" (*isa2*) walther@60318: ####### calc. to: False (*isa*) walther@60318: True (*isa2*) walther@60318: ( **) walther@60318: if is_addUnordered (TermC.str2term "x \ 2 * y \ 2 + x \ 3 * y ::real") then () walther@60318: else error"is_addUnordered x \ 2 * y \ 2 + x \ 3 * y"; (*isa == isa2*) walther@60318: "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \ 2 * y \ 2 + x \ 3 * y ::real"); walther@60318: ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*) walther@60318: walther@60318: (*+*) if is_polyexp t = true then () else error "is_polyexp x \ 2 * y \ 2 + x \ 3 * y"; walther@60318: walther@60318: (*+*) if t = sort_monoms t = false then () else error "sort_monoms 123"; walther@60318: "~~~~~~~ fun sort_monoms , args:"; val (t) = (t); walther@60318: val ll = map monom2list (poly2list t); walther@60318: val lls = sort_monList ll; walther@60318: walther@60318: (*+*)map UnparseC.terms lls = ["[\"x \ 2\", \"y \ 2\"]", "[\"x \ 3\", \"y\"]"]; (*isa*) walther@60318: (*+*)map UnparseC.terms lls = ["[\"x \ 3\", \"y\"]", "[\"x \ 2\", \"y \ 2\"]"]; (*isa2*) walther@60318: walther@60318: "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = (); walther@60318: (* we check all elements at once..*) walther@60318: val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \ 2\", \"y \ 2\"]"; walther@60318: val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \ 3\", \"y\"]"; walther@60318: walther@60318: (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED"; walther@60318: (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED"; walther@60318: (*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*) walther@60318: (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED"; walther@60318: (* isa -- isa2: walther@60318: (*1*){a = "var_ord_revPow ", at_bt = "(x \ 2, x \ 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*) walther@60318: (*1*){a = "var_ord_revPow ", at_bt = "(y \ 2, y \ 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*) walther@60318: (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \ 2\", \"y \ 2\"], [\"x \ 2\", \"y \ 2\"])", sort_args = "(---, ---)"} (*isa == isa2*) walther@60318: walther@60318: (*2*){a = "var_ord_revPow ", at_bt = "(x \ 2, x \ 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*) walther@60318: walther@60318: (*3*)k{a = "var_ord_revPow ", at_bt = "(x \ 3, x \ 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*) walther@60318: walther@60318: (*4*){a = "var_ord_revPow ", at_bt = "(x \ 3, x \ 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*) walther@60318: (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*) walther@60318: (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \ 3\", \"y\"], [\"x \ 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*) walther@60318: val it = true: bool walther@60318: val it = true: bool walther@60318: val it = true: bool walther@60318: val it = true: bool*) walther@60318: walther@60318: "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = (); walther@60318: (*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED"; walther@60318: (*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*) walther@60318: (*{a = "int_ord (4, 10003) = ", z = LESS} isa walther@60318: {a = "int_ord (4, 4) = ", z = EQUAL} isa2*) walther@60318: (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*) walther@60318: (*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED"; walther@60318: (* isa -- isa2: walther@60318: (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*) walther@60318: {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) walther@60318: (*1*){a = "dict_cond_ord", args = "([\"x \ 2\", \"y \ 2\"], [\"x \ 2\", \"y \ 2\"])", is_nums = "(false, false)"} (*isa*) walther@60318: (*1*){a = "var_ord_revPow ", at_bt = "(x \ 2, x \ 2)", sort_args = "(x, 2), (x, 2)"} (*isa*) walther@60318: (*1*){a = "dict_cond_ord", args = "([\"y \ 2\"], [\"y \ 2\"])", is_nums = "(false, false)"} (*isa*) walther@60318: (*1*){a = "var_ord_revPow ", at_bt = "(y \ 2, y \ 2)", sort_args = "(y, 2), (y, 2)"} (*isa*) walther@60318: (*1*){a = "dict_cond_ord ([], [])"} (*isa*) walther@60318: walther@60318: (*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*) walther@60318: {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) walther@60318: {a = "dict_cond_ord", args = "([\"x \ 2\", \"y \ 2\"], [\"x \ 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*) walther@60318: (*2*){a = "var_ord_revPow ", at_bt = "(x \ 2, x \ 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*) walther@60318: walther@60318: (*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*) walther@60318: {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) walther@60318: {a = "dict_cond_ord", args = "([\"x \ 3\", \"y\"], [\"x \ 2\", \"y \ 2\"])", is_nums = "(false, false)"} walther@60318: (*3*){a = "var_ord_revPow ", at_bt = "(x \ 3, x \ 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*) walther@60318: walther@60318: (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*) walther@60318: {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) walther@60318: (*4*){a = "dict_cond_ord", args = "([\"x \ 3\", \"y\"], [\"x \ 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*) walther@60318: (*4*){a = "var_ord_revPow ", at_bt = "(x \ 3, x \ 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*) walther@60318: (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*) walther@60318: (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*) walther@60318: (*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*) walther@60318: walther@60318: val it = true: bool walther@60318: val it = false: bool walther@60318: val it = false: bool walther@60318: val it = true: bool walther@60318: *) walther@60318: walther@60318: (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \ 2\", \"y \ 2\"] CHANGED"; walther@60318: "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1); walther@60318: "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* ) walther@60318: (*if*) (is_nums x) (*else*); walther@60318: val (Const ("Transcendental.powr", _) $ Free _ $ t) = walther@60318: (*case*) x (*of*); walther@60318: (*+*)UnparseC.term x = "x \ 2"; walther@60318: (*if*) TermC.is_num t (*then*); walther@60318: walther@60318: counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); walther@60318: "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs); walther@60318: (*if*) (is_nums x) (*else*); walther@60318: val (Const ("Transcendental.powr", _) $ Free _ $ t) = walther@60318: (*case*) x (*of*); walther@60318: (*+*)UnparseC.term x = "y \ 2"; walther@60318: (*if*) TermC.is_num t (*then*); walther@60318: walther@60318: val return = walther@60318: counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); walther@60318: if return = 4 then () else error "monom_degree [\"x \ 2\", \"y \ 2\"] CHANGED"; walther@60318: ( *---------------------------------------------------------------------------------OPEN local/*) walther@60318: walther@60318: (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then () walther@60318: else error "monom_degree [\"x \ 3\", \"y\"] CHANGED"; walther@60318: "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2); walther@60318: "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* ) walther@60318: (*if*) (is_nums x) (*else*); walther@60318: val (Const ("Transcendental.powr", _) $ Free _ $ t) = walther@60318: (*case*) x (*of*); walther@60318: (*+*)UnparseC.term x = "x \ 3"; walther@60318: (*if*) TermC.is_num t (*then*); walther@60318: walther@60318: counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); walther@60318: "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs); walther@60318: (*if*) (is_nums x) (*else*); walther@60318: val _ = (*the default case*) walther@60318: (*case*) x (*of*); walther@60318: ( *---------------------------------------------------------------------------------OPEN local/*) walther@60318: walther@60318: "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = (); walther@60318: val xxx = dict_cond_ord var_ord_revPow is_nums; walther@60318: (*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED"; walther@60318: (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED"; walther@60318: (*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED"; walther@60318: (*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED"; walther@60318: walther@60318: walther@60318: "-------- check make_polynomial with simple terms ----------------------------------------------"; walther@60318: "-------- check make_polynomial with simple terms ----------------------------------------------"; walther@60318: "-------- check make_polynomial with simple terms ----------------------------------------------"; neuper@38036: "----- check 1 ---"; walther@60230: val t = TermC.str2term "2*3*a"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1"; neuper@38036: neuper@38036: "----- check 2 ---"; walther@60230: val t = TermC.str2term "2*a + 3*a"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2"; neuper@38036: neuper@38036: "----- check 3 ---"; walther@60230: val t = TermC.str2term "2*a + 3*a + 3*a"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3"; neuper@38036: neuper@38036: "----- check 4 ---"; walther@60230: val t = TermC.str2term "3*a - 2*a"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "a" then () else error "check make_polynomial 4"; neuper@38036: neuper@38036: "----- check 5 ---"; walther@60230: val t = TermC.str2term "4*(3*a - 2*a)"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5"; neuper@38036: neuper@38036: "----- check 6 ---"; walther@60242: val t = TermC.str2term "4*(3*a \ 2 - 2*a \ 2)"; neuper@38036: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; walther@60242: if UnparseC.term t = "4 * a \ 2" then () else error "check make_polynomial 6"; neuper@38036: walther@60318: "-------- fun is_multUnordered (x \ 2 * x) -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x \ 2 * x) -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x \ 2 * x) -----------------------------------------------------"; wneuper@59592: val thy = @{theory "Isac_Knowledge"}; neuper@38040: "===== works for a simple example, see rewrite.sml -- fun app_rev ==="; walther@60242: val t = TermC.str2term "x \ 2 * x"; neuper@38040: val SOME (t', _) = rewrite_set_ thy true order_mult_ t; walther@60242: if UnparseC.term t' = "x * x \ 2" then () walther@60278: else error "poly.sml Poly.is_multUnordered doesn't work"; neuper@38040: walther@59901: (* 100928 Rewrite.trace_on shows the first occurring difference in 267b: walther@60242: ### rls: order_mult_ on: 5 * x \ 2 * (2 * x \ 7) + 5 * x \ 2 * 3 + (6 * x \ 7 + 9) + (-1 * (3 * x \ 5 * (6 * x \ 4)) + -1 * (3 * x \ 5 * -1) + walther@60242: (-48 * x \ 4 + 8)) walther@59852: ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered walther@60278: ####### try calc: Poly.is_multUnordered' neuper@38036: ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!! neuper@38036: *) walther@60242: val t = TermC.str2term "5 * x \ 2 * (2 * x \ 7) + 5 * x \ 2 * 3 + (6 * x \ 7 + 9) + (-1 * (3 * x \ 5 * (6 * x \ 4)) + -1 * (3 * x \ 5 * -1) + (-48 * x \ 4 + 8))"; neuper@38036: neuper@38036: "----- is_multUnordered ---"; neuper@38036: val tsort = sort_variables t; walther@60242: UnparseC.term tsort = "2 * (5 * (x \ 2 * x \ 7)) + 3 * (5 * x \ 2) + 6 * x \ 7 + 9 +\n-1 * (3 * (6 * (x \ 4 * x \ 5))) +\n-1 * (-1 * (3 * x \ 5)) +\n-48 * x \ 4 +\n8"; neuper@38036: is_polyexp t; neuper@38036: tsort = t; neuper@38036: is_polyexp t andalso not (t = sort_variables t); neuper@38036: if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1"; neuper@38036: neuper@38036: "----- eval_is_multUnordered ---"; walther@60242: val tm = TermC.str2term "(5 * x \ 2 * (2 * x \ 7) + 5 * x \ 2 * 3 + (6 * x \ 7 + 9) + (-1 * (3 * x \ 5 * (6 * x \ 4)) + -1 * (3 * x \ 5 * -1) + (-48 * x \ 4 + 8))) is_multUnordered"; neuper@38036: case eval_is_multUnordered "testid" "" tm thy of neuper@41924: SOME (_, Const ("HOL.Trueprop", _) $ neuper@41922: (Const ("HOL.eq", _) $ walther@60278: (Const ("Poly.is_multUnordered", _) $ _) $ neuper@41928: Const ("HOL.True", _))) => () neuper@38036: | _ => error "poly.sml diff. eval_is_multUnordered"; neuper@38036: neuper@38040: "----- rewrite_set_ STILL DIDN'T WORK"; neuper@38040: val SOME (t, _) = rewrite_set_ thy true order_mult_ t; walther@59868: UnparseC.term t; neuper@38036: walther@60318: walther@60318: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; walther@60318: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; walther@60318: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; walther@60318: val thy = @{theory "Isac_Knowledge"}; walther@60318: val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered"; walther@60318: walther@60318: (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true walther@60318: (*+*) andalso not (is_multUnordered arg) walther@60318: (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED"; walther@60318: walther@60318: case eval_is_multUnordered "xxx " "yyy " t thy of walther@60318: SOME walther@60318: ("xxx 3 * a + - 2 * a_", walther@60318: Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ walther@60318: Const ("HOL.False", _))) => () walther@60318: (* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*) walther@60318: | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; walther@60318: walther@60318: "----- is_multUnordered --- (- 2 * a) is_multUnordered = False"; walther@60318: val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered"; walther@60318: walther@60318: (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true walther@60318: (*+*) andalso not (is_multUnordered arg) walther@60318: (*+*)then () else error "sort_variables - 2 * a CHANGED"; walther@60318: walther@60318: case eval_is_multUnordered "xxx " "yyy " t thy of walther@60318: SOME walther@60318: ("xxx - 2 * a_", walther@60318: Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ walther@60318: Const ("HOL.False", _))) => () walther@60318: | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; walther@60318: walther@60318: "----- is_multUnordered --- (a) is_multUnordered = False"; walther@60318: val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered"; walther@60318: walther@60318: (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true walther@60318: (*+*) andalso not (is_multUnordered arg) walther@60318: (*+*)then () else error "sort_variables a CHANGED"; walther@60318: walther@60318: case eval_is_multUnordered "xxx " "yyy " t thy of walther@60318: SOME walther@60318: ("xxx a_", walther@60318: Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ walther@60318: Const ("HOL.False", _))) => () walther@60318: | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; walther@60318: walther@60318: "----- is_multUnordered --- (- 2) is_multUnordered = False"; walther@60318: val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered"; walther@60318: walther@60318: (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true walther@60318: (*+*) andalso not (is_multUnordered arg) walther@60318: (*+*)then () else error "sort_variables - 2 CHANGED"; walther@60318: walther@60318: case eval_is_multUnordered "xxx " "yyy " t thy of walther@60318: SOME walther@60318: ("xxx - 2_", walther@60318: Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ walther@60318: Const ("HOL.False", _))) => () walther@60318: | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; walther@60318: walther@60318: walther@60318: "-------- fun is_multUnordered (x - a) \ 3 -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x - a) \ 3 -----------------------------------------------------"; walther@60318: "-------- fun is_multUnordered (x - a) \ 3 -----------------------------------------------------"; walther@60318: (* ca.line 45 of Rewrite.trace_on: walther@60318: ## rls: order_mult_rls_ on: walther@60318: x \ 3 + 3 * x \ 2 * (- 1 * a) + 3 * x * ((- 1) \ 2 * a \ 2) + (- 1) \ 3 * a \ 3 walther@60318: ### rls: order_mult_ on: walther@60318: x \ 3 + 3 * x \ 2 * (- 1 * a) + 3 * x * ((- 1) \ 2 * a \ 2) + (- 1) \ 3 * a \ 3 walther@60318: ###### rls: Rule_Set.empty-is_multUnordered on: walther@60318: x \ 3 + 3 * x \ 2 * (- 1 * a) + 3 * x * ((- 1) \ 2 * a \ 2) + (- 1) \ 3 * a \ 3 is_multUnordered walther@60318: ####### try calc: "Poly.is_multUnordered" walther@60318: ######## eval asms: walther@60318: N:x \ 3 + 3 * x \ 2 * (- 1 * a) + 3 * x * ((- 1) \ 2 * a \ 2) + (- 1) \ 3 * a \ 3 is_multUnordered = True" walther@60318: -------------------------------------------------------------------------------------------------== walther@60318: O:x \ 3 + 3 * x \ 2 * (-1 * a) + 3 * x * (-1 \ 2 * a \ 2) + -1 \ 3 * a \ 3 is_multUnordered = True" walther@60318: ####### calc. to: True walther@60318: ####### try calc: "Poly.is_multUnordered" walther@60318: ####### try calc: "Poly.is_multUnordered" walther@60318: ### rls: order_mult_ on: walther@60318: N:x \ 3 + - 1 * (3 * (a * x \ 2)) + 3 * (a \ 2 * (x * (- 1) \ 2)) + a \ 3 * (- 1) \ 3 walther@60318: --------+--------------------------+---------------------------------+---------------------------<> walther@60318: O:x \ 3 + -1 * (3 * (a * x \ 2)) + -1 \ 2 * (3 * (a \ 2 * x)) + -1 \ 3 * a \ 3 walther@60318: -------------------------------------------------------------------------------------------------<> walther@60318: *) walther@60318: val t = TermC.str2term "x \ 3 + 3 * x \ 2 * (- 1 * a) + 3 * x * ((- 1) \ 2 * a \ 2) + (- 1) \ 3 * a \ 3"; walther@60318: (* walther@60318: "~~~~~ fun is_multUnordered walther@60318: "~~~~~~~ fun sort_variables walther@60318: "~~~~~~~~~ val sort_varList walther@60318: *) walther@60318: "~~~~~ fun is_multUnordered , args:"; val (t) = (t); walther@60318: is_polyexp t = true; walther@60318: walther@60318: val return = walther@60318: sort_variables t; walther@60318: (*+*)if UnparseC.term return = walther@60318: (*+*) "x \ 3 + - 1 * (3 * (a * x \ 2)) +\n(- 1) \ 2 * (3 * (a \ 2 * x)) +\n(- 1) \ 3 * a \ 3" walther@60318: (*+*)then () else error "sort_variables x \ 3 + - 1 * (3 * (a * x \ 2)) .. CHANGED"; walther@60318: walther@60318: "~~~~~~~ fun sort_variables , args:"; val (t) = (t); walther@60318: val ll = map monom2list (poly2list t); walther@60318: val lls = map sort_varList ll; walther@60318: walther@60318: (*+*)val ori3 = nth 3 ll; walther@60318: (*+*)val mon3 = nth 3 lls; walther@60318: walther@60318: (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \ 3\"]" then () else error "nth 1 ll"; walther@60318: (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \ 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll"; walther@60318: (*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \ 2\", \"a \ 2\"]" then () else error "nth 3 ll"; walther@60318: (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \ 3\", \"a \ 3\"]" then () else error "nth 4 ll"; walther@60318: walther@60318: (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \ 3\"]" then () else error "nth 1 lls"; walther@60318: (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \ 2\"]" then () else error "nth 2 lls"; walther@60318: (*+*)if UnparseC.terms mon3 = "[\"(- 1) \ 2\", \"3\", \"a \ 2\", \"x\"]" then () else error "nth 3 lls"; walther@60318: (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \ 3\", \"a \ 3\"]" then () else error "nth 4 lls"; walther@60318: walther@60318: "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3); walther@60318: (* Output below with: walther@60318: val sort_varList = sort var_ord; walther@60318: fun var_ord (a,b: term) = walther@60318: (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", walther@60318: sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; walther@60318: prod_ord string_ord string_ord walther@60318: ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) walther@60318: ); walther@60318: *) walther@60318: (*+*)val xxx = sort_varList ori3; walther@60318: (* walther@60318: {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \ 2\", \"a \ 2\"]"} (*isa*) walther@60318: {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \ 2\", \"a \ 2\"]"} (*isa2*) walther@60318: walther@60318: isa isa2 walther@60318: {a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"} walther@60318: {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"} walther@60318: {a = "var_ord ", a_b = "(x, (- 1) \ 2)"} {a = "var_ord ", a_b = "(x, (- 1) \ 2)"} walther@60318: {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"} walther@60318: {a = "var_ord ", a_b = "((- 1) \ 2, a \ 2)"} {a = "var_ord ", a_b = "((- 1) \ 2, a \ 2)"} walther@60318: {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"} walther@60318: ^^^ ^^^ walther@60318: walther@60318: {a = "var_ord ", a_b = "(x, a \ 2)"} {a = "var_ord ", a_b = "(x, a \ 2)"} walther@60318: {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"} walther@60318: ^^^ ^^^ walther@60318: {a = "var_ord ", a_b = "(x, (- 1) \ 2)"} {a = "var_ord ", a_b = "(x, (- 1) \ 2)"} walther@60318: {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"} walther@60318: {a = "var_ord ", a_b = "(3, (- 1) \ 2)"} {a = "var_ord ", a_b = "(3, (- 1) \ 2)"} walther@60318: {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"} walther@60318: *) walther@60318: walther@60318: walther@60318: "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; walther@60318: "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; walther@60318: "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; walther@60318: val t = TermC.str2term "b * a * a"; walther@60318: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "a \ 2 * b" then () walther@60318: else error "poly.sml: diff.behav. in make_polynomial 21"; walther@60318: walther@60318: "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"}); walther@60318: ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*) walther@60318: walther@60318: (*+*)if is_polyexp t then () else error "is_polyexp a \ 2 * b CHANGED"; walther@60318: "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t); walther@60318: (*if*) TermC.is_num num (*else*); walther@60318: walther@60318: "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num); walther@60318: (*if*) TermC.is_num num (*else*); walther@60318: (*if*) TermC.is_variable num (*then*); walther@60318: walther@60318: val xxx = sort_variables t; walther@60318: (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \ 2 * b CHANGED"; walther@60318: walther@60318: walther@60318: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; walther@60318: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; walther@60318: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; walther@60318: val t = TermC.str2term "2*3*a"; walther@60318: val SOME (t', _) = rewrite_set_ thy false make_polynomial t; walther@60318: (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED"; walther@60318: (* walther@60318: ## try calc: "Groups.times_class.times" walther@60318: ## rls: order_mult_rls_ on: 6 * a walther@60318: ### rls: order_mult_ on: 6 * a walther@60318: ###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered walther@60318: ####### try calc: "Poly.is_multUnordered" walther@60318: ######## eval asms: "6 * a is_multUnordered = True" (*isa*) walther@60318: = False" (*isa2*) walther@60318: ####### calc. to: True (*isa*) walther@60318: False (*isa2*) walther@60318: *) walther@60318: val t = TermC.str2term "(6 * a) is_multUnordered"; walther@60318: val SOME walther@60318: (_, t') = walther@60318: eval_is_multUnordered "xxx" () t @{theory}; walther@60318: (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () walther@60318: (*+*)else error "6 * a is_multUnordered = False CHANGED"; walther@60318: walther@60318: "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _, walther@60318: (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory}); walther@60318: (*if*) is_multUnordered arg (*else*); walther@60318: walther@60318: "~~~~~ fun is_multUnordered , args:"; val (t) = (arg); walther@60318: val return = walther@60318: ((is_polyexp t) andalso not (t = sort_variables t)); walther@60318: walther@60318: (*+*)return = false; (*isa*) walther@60318: (*+*) is_polyexp t = true; (*isa*) walther@60318: (*+*) not (t = sort_variables t) = false; (*isa*) walther@60318: walther@60318: val xxx = sort_variables t; walther@60318: (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED"; walther@60318: walther@60318: walther@60318: "-------- examples from textbook Schalk I ------------------------------------------------------"; walther@60318: "-------- examples from textbook Schalk I ------------------------------------------------------"; walther@60318: "-------- examples from textbook Schalk I ------------------------------------------------------"; neuper@38036: "-----SPB Schalk I p.63 No.267b ---"; walther@60242: val t = TermC.str2term "(5*x \ 2 + 3) * (2*x \ 7 + 3) - (3*x \ 5 + 8) * (6*x \ 4 - 1)"; walther@60318: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "17 + 15 * x \ 2 + - 48 * x \ 4 + 3 * x \ 5 + 6 * x \ 7 +\n- 8 * x \ 9" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 1"; neuper@37906: neuper@38036: "-----SPB Schalk I p.63 No.275b ---"; walther@60242: val t = TermC.str2term "(3*x \ 2 - 2*x*y + y \ 2) * (x \ 2 - 2*y \ 2)"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = walther@60318: "3 * x \ 4 + - 2 * x \ 3 * y + - 5 * x \ 2 * y \ 2 +\n4 * x * y \ 3 +\n- 2 * y \ 4" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 2"; neuper@37906: neuper@38036: "-----SPB Schalk I p.63 No.279b ---"; walther@60230: val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = walther@60318: ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \ 2 +\n" ^ walther@60318: "- 1 * a * c * d * x +\na * c * x \ 2 +\na * d * x \ 2 +\n- 1 * a * x \ 3 +\n" ^ walther@60318: "- 1 * b * c * d * x +\nb * c * x \ 2 +\nb * d * x \ 2 +\n- 1 * b * x \ 3 +\nc" ^ walther@60318: " * d * x \ 2 +\n- 1 * c * x \ 3 +\n- 1 * d * x \ 3 +\nx \ 4") neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 3"; walther@60318: (*associate poly*) neuper@37906: neuper@38036: "-----SPB Schalk I p.63 No.291 ---"; walther@60242: val t = TermC.str2term "(5+96*x \ 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = "50 + - 770 * x + 4520 * x \ 2 + - 16320 * x \ 3 +\n- 26880 * x \ 4" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 4"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.295c ---"; walther@60242: val t = TermC.str2term "(13*a \ 4*b \ 9*c - 12*a \ 3*b \ 6*c \ 9) \ 2"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = walther@60318: "169 * a \ 8 * b \ 18 * c \ 2 +\n- 312 * a \ 7 * b \ 15 * c \ 10 +\n144 * a \ 6 * b \ 12 * c \ 18" neuper@42395: then ()else error "poly.sml: diff.behav. in make_polynomial 5"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.299a ---"; walther@60230: val t = TermC.str2term "(x - y)*(x + y)"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = "x \ 2 + - 1 * y \ 2" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 6"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.300c ---"; walther@60242: val t = TermC.str2term "(3*x \ 2*y - 1)*(3*x \ 2*y + 1)"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@60318: if UnparseC.term t = "- 1 + 9 * x \ 4 * y \ 2" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 7"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.302 ---"; walther@60230: val t = TermC.str2term walther@60242: "(13*x \ 2 + 5)*(13*x \ 2 - 5) - (5*x \ 2 + 3)*(5*x \ 2 - 3) - (12*x \ 2 + 4)*(12*x \ 2 - 4)"; neuper@42395: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; walther@59868: if UnparseC.term t = "0" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 8"; neuper@42395: (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *) neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.306a ---"; walther@60242: val t = TermC.str2term "((x \ 2 + 1)*(x \ 2 - 1)) \ 2"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "1 + 2 * x \ 4 + 2 * - 2 * x \ 4 + x \ 8" then () walther@60242: else error "poly.sml: diff.behav. in 2 * x \ 4 + 2 * -2 * x \ 4 = -2 * x \ 4"; neuper@37906: neuper@37906: (*WN071729 when reducing "rls reduce_012_" for Schaerding, neuper@37906: the above resulted in the term below ... but reduces from then correctly*) walther@60242: val t = TermC.str2term "1 + 2 * x \ 4 + 2 * -2 * x \ 4 + x \ 8"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "1 + - 2 * x \ 4 + x \ 8" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 9b"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.296a ---"; walther@60242: val t = TermC.str2term "(x - a) \ 3"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: walther@60318: val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc"; walther@60318: walther@60318: if UnparseC.term t = "- 1 * a \ 3 + 3 * a \ 2 * x + - 3 * a * x \ 2 + x \ 3" neuper@38031: then () else error "poly.sml: diff.behav. in make_polynomial 10"; neuper@37906: neuper@38036: "-----SPB Schalk I p.64 No.296c ---"; walther@60242: val t = TermC.str2term "(-3*x - 4*y) \ 3"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "- 27 * x \ 3 + - 108 * x \ 2 * y + - 144 * x * y \ 2 +\n- 64 * y \ 3" neuper@38031: then () else error "poly.sml: diff.behav. in make_polynomial 11"; neuper@37906: neuper@38036: "-----SPB Schalk I p.62 No.242c ---"; walther@60242: val t = TermC.str2term "x \ (-4)*(x \ (-4)*y \ (-2)) \ (-1)*y \ (-2)"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "1" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 12"; neuper@37906: neuper@38036: "-----SPB Schalk I p.60 No.209a ---"; walther@60242: val t = TermC.str2term "a \ (7-x) * a \ x"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "a \ 7" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 13"; neuper@37906: neuper@38036: "-----SPB Schalk I p.60 No.209d ---"; walther@60242: val t = TermC.str2term "d \ x * d \ (x+1) * d \ (2 - 2*x)"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "d \ 3" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 14"; neuper@37906: walther@60318: "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------"; walther@60318: "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------"; walther@60318: "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------"; neuper@38036: "-----Schalk I p.64 No.303 ---"; walther@60242: val t = TermC.str2term "(a + 2*b)*(a \ 2 + 4*b \ 2)*(a - 2*b) - (a - 6*b)*(a \ 2 + 36*b \ 2)*(a + 6*b)"; walther@60318: (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*) walther@60318: val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "1280 * b \ 4" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 14b"; neuper@37906: (* Richtig - aber Binomische Formel wurde nicht verwendet! *) walther@60318: (*SOMETIMES LOOPS--------------------------------------------------------------------------//*) neuper@37906: walther@60318: "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------"; walther@60318: "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------"; walther@60318: "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "a \ 2*a \ (-2)"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@59868: if UnparseC.term t = "1" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 15"; neuper@38036: "-----SPO ---"; walther@60230: val t = TermC.str2term "a + a + a"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@59868: if UnparseC.term t = "3 * a" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 16"; neuper@38036: "-----SPO ---"; walther@60230: val t = TermC.str2term "a + b + b + b"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@59868: if UnparseC.term t = "a + 3 * b" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 17"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "a \ 2*b*b \ (-1)"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "a \ 2" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 18"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "a \ 2*a \ (-2)"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@59868: if (UnparseC.term t) = "1" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 19"; neuper@38036: "-----SPO ---"; walther@60230: val t = TermC.str2term "b + a - b"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@59868: if (UnparseC.term t) = "a" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 20"; neuper@38036: "-----SPO ---"; walther@60230: val t = TermC.str2term "b * a * a"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "a \ 2 * b" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 21"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "(a \ 2) \ 3"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "a \ 6" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 22"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "x \ 2 * y \ 2 + x * x \ 2 * y"; walther@59868: val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; walther@60242: if UnparseC.term t = "x \ 3 * y + x \ 2 * y \ 2" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 23"; neuper@38036: "-----SPO ---"; walther@60242: val t = (Thm.term_of o the o (TermC.parse thy)) "a \ 2 * (-a) \ 2"; walther@60318: val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t; walther@60242: if (UnparseC.term t) = "a \ 4" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 24"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "a * b * b \ (-1) + a"; walther@60318: val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "2 * a" then () neuper@38031: else error "poly.sml: diff.behav. in make_polynomial 25"; neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "a*c*b \ (2*n) + 3*a + 5*b \ (2*n)*c*b"; walther@60318: val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t; walther@60318: if UnparseC.term t = "3 * a + 5 * b \ (1 + 2 * n) * c + a * b \ (2 * n) * c" neuper@38031: then () else error "poly.sml: diff.behav. in make_polynomial 26"; neuper@37906: neuper@42395: (*MG030627 -------------vvv-: Verschachtelte Terme -----------*) neuper@38036: "-----SPO ---"; walther@60242: val t = TermC.str2term "(1 + (x*y*a) + x) \ (1 + (x*y*a) + x)"; walther@60318: val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; walther@60242: if UnparseC.term t = "(1 + x + a * x * y) \ (1 + x + a * x * y)" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*) neuper@42395: walther@60242: val t = TermC.str2term "(1 + x*(y*z)*zz) \ (1 + x*(y*z)*zz)"; walther@60318: val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; walther@60242: if UnparseC.term t = "(1 + x * y * z * zz) \ (1 + x * y * z * zz)" neuper@42395: then () else error "poly.sml: diff.behav. in make_polynomial 28"; neuper@37906: walther@60318: "-------- check pbl 'polynomial simplification' -----------------------------------------------"; walther@60318: "-------- check pbl 'polynomial simplification' -----------------------------------------------"; walther@60318: "-------- check pbl 'polynomial simplification' -----------------------------------------------"; walther@60242: val fmz = ["Term ((5*x \ 2 + 3) * (2*x \ 7 + 3) - (3*x \ 5 + 8) * (6*x \ 4 - 1))", "normalform N"]; neuper@38036: "-----0 ---"; walther@60318: case Refine.refine fmz ["polynomial", "simplification"] of walther@59984: [M_Match.Matches (["polynomial", "simplification"], _)] => () walther@59968: | _ => error "poly.sml diff.behav. in check pbl, Refine.refine"; neuper@37906: (*...if there is an error, then ...*) neuper@37906: neuper@38036: "-----1 ---"; wneuper@59348: (*default_print_depth 7;*) walther@59997: val pbt = Problem.from_store ["polynomial", "simplification"]; wneuper@59348: (*default_print_depth 3;*) neuper@37906: (*if there is ... walther@59984: > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt; walther@59901: ... then Rewrite.trace_on:*) walther@60242: neuper@38036: "-----2 ---"; walther@59901: Rewrite.trace_on := false; walther@59984: M_Match.match_pbl fmz pbt; walther@59901: Rewrite.trace_on := false; neuper@37906: (*... if there is no rewrite, then there is something wrong with prls*) neuper@52101: neuper@38036: "-----3 ---"; wneuper@59348: (*default_print_depth 7;*) walther@59997: val prls = (#prls o Problem.from_store) ["polynomial", "simplification"]; wneuper@59348: (*default_print_depth 3;*) walther@60242: val t = TermC.str2term "((5*x \ 2 + 3) * (2*x \ 7 + 3) - (3*x \ 5 + 8) * (6*x \ 4 - 1)) is_polyexp"; neuper@37926: val SOME (t',_) = rewrite_set_ thy false prls t; neuper@48760: if t' = @{term True} then () neuper@38031: else error "poly.sml: diff.behav. in check pbl 'polynomial.."; neuper@42395: (*... if this works, but --1-- does still NOT work, check types:*) neuper@37906: neuper@38036: "-----4 ---"; neuper@42395: (*show_types:=true;*) neuper@37906: (* walther@59984: > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt; neuper@37906: val wh = [False "(t_::real => real) (is_polyexp::real)"] walther@60242: ...................... \ \ \ \ ............... \ ^*) walther@59984: val M_Match.Matches' _ = M_Match.match_pbl fmz pbt; neuper@42395: (*show_types:=false;*) neuper@37906: walther@59787: walther@60318: "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------"; walther@60318: "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------"; walther@60318: "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------"; walther@60242: val fmz = ["Term ((5*x \ 2 + 3) * (2*x \ 7 + 3) - (3*x \ 5 + 8) * (6*x \ 4 - 1))", "normalform N"]; neuper@37906: val (dI',pI',mI') = walther@59997: ("Poly",["polynomial", "simplification"], walther@59997: ["simplification", "for_polynomials"]); neuper@37906: val p = e_pos'; val c = []; neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; walther@60242: (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \ 2 + 3) * (2 * x \ 7 + 3) -\n (3 * x \ 5 + 8) * (6 * x \ 4 - 1))"*) walther@59787: (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*) walther@59787: walther@59997: (*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) = walther@60242: (*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \ 2 + 3) * (2 * x \ 7 + 3) -\n (3 * x \ 5 + 8) * (6 * x \ 4 - 1)) ,(t_t, [(5 * x \ 2 + 3) * (2 * x \ 7 + 3) -\n(3 * x \ 5 + 8) * (6 * x \ 4 - 1)]))]" walther@59943: (*+*)then () else error "No.267b: I_Model.T CHANGED"; walther@59997: ( *+ ...could not be repaired in child of 7e314dd233fd ?!?*) walther@59787: walther@59787: (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*) walther@59787: (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*) walther@59787: (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*) walther@59787: (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*) walther@59787: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*) walther@59787: walther@60242: (*+*)if f2str f = "(5 * x \ 2 + 3) * (2 * x \ 7 + 3) -\n(3 * x \ 5 + 8) * (6 * x \ 4 - 1)" walther@59787: (*+*)then () else error ""; walther@59787: walther@59787: (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*) walther@59787: walther@60318: (*+*)if f2str f = "17 + 15 * x \ 2 + - 48 * x \ 4 + 3 * x \ 5 + 6 * x \ 7 +\n- 8 * x \ 9" walther@60248: (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1"; walther@59787: walther@59790: (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*) walther@59787: walther@59787: neuper@37906: walther@60318: "-------- interSteps for Schalk 299a -----------------------------------------------------------"; walther@60318: "-------- interSteps for Schalk 299a -----------------------------------------------------------"; walther@60318: "-------- interSteps for Schalk 299a -----------------------------------------------------------"; s1210629013@55445: reset_states (); neuper@37906: CalcTree neuper@42395: [(["Term ((x - y)*(x + (y::real)))", "normalform N"], walther@59997: ("Poly",["polynomial", "simplification"], walther@59997: ["simplification", "for_polynomials"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; walther@59983: val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; neuper@37906: walther@59833: interSteps 1 ([1],Res)(* syserror in Detail_Step.go *); walther@59983: val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; neuper@37906: if existpt' ([1,1], Frm) pt then () neuper@38031: else error "poly.sml: interSteps doesnt work again 1"; neuper@37906: walther@59833: interSteps 1 ([1,1],Res)(* syserror in Detail_Step.go *); walther@59983: val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; neuper@42395: (*============ inhibit exn WN120316 ============================================== neuper@37906: if existpt' ([1,1,1], Frm) pt then () neuper@38031: else error "poly.sml: interSteps doesnt work again 2"; neuper@42395: ============ inhibit exn WN120316 ==============================================*) neuper@37906: walther@60318: "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------"; walther@60318: "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------"; walther@60318: "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------"; walther@60267: val thy = @{theory AlgEin}; wneuper@59529: wneuper@59529: val SOME (f',_) = rewrite_set_ thy false norm_Poly walther@60230: (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben"); walther@60318: if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben" neuper@42395: then ((*norm_Poly NOT COMPLETE -- TODO MG*)) neuper@42395: else error "norm_Poly changed behavior"; walther@60318: (* isa: walther@60318: ## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben walther@60318: ### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben walther@60318: ###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + walther@60318: oben is_addUnordered walther@60318: ####### try calc: "Poly.is_addUnordered" walther@60318: ######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + walther@60318: oben is_addUnordered = True" walther@60318: ####### calc. to: True walther@60318: ####### try calc: "Poly.is_addUnordered" walther@60318: ####### try calc: "Poly.is_addUnordered" walther@60318: ### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben walther@60318: *) walther@60318: "~~~~~ fun sort_monoms , args:"; val (t) = walther@60318: (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"); walther@60318: (*+*)val t' = walther@60318: sort_monoms t; walther@60318: (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*) neuper@38036: walther@60318: "-------- ord_make_polynomial ------------------------------------------------------------------"; walther@60318: "-------- ord_make_polynomial ------------------------------------------------------------------"; walther@60318: "-------- ord_make_polynomial ------------------------------------------------------------------"; walther@60230: val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)"; walther@60318: val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b"; neuper@37906: neuper@42395: if ord_make_polynomial true thy [] (t1, t2) then () neuper@38031: else error "poly.sml: diff.behav. in ord_make_polynomial"; walther@60318: (*SO: WHY IS THERE NO REWRITING ...*) neuper@37906: walther@60230: val term = TermC.str2term "2*b + (3*a + 3*b)"; walther@60325: (*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term; walther@60325: (* walther@60325: WHY IS THERE NO REWRITING ?!? walther@60325: most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML, walther@60325: while order_add_mult uses isac's rewriter -- and this is used rarely! walther@60318: *) neuper@37906: