(* testexamples for Poly, polynomials

   author: Matthias Goldgruber 2003

   (c) due to copyright terms

LEGEND:

WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'

          examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'

*)

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";

"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";

"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";

"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";

"-------- investigate (new 2002) uniary minus --------------------------------------------------";

"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";

"-------- examples from textbook Schalk I ------------------------------------------------------";

"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";

"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";

"-------- check pbl  'polynomial simplification' -----------------------------------------------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";

"-------- interSteps for Schalk 299a -----------------------------------------------------------";

"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";

"-------- ord_make_polynomial ------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";

"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";

"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";

(* indentation indicates call hierarchy:

"~~~~~ fun is_addUnordered

"~~~~~~~ fun is_polyexp

"~~~~~~~ fun sort_monoms

"~~~~~~~~~ fun sort_monList

"~~~~~~~~~~~ fun koeff_degree_ord    : term list * term list -> order

"~~~~~~~~~~~~~ fun degree_ord        : term list * term list -> order

"~~~~~~~~~~~~~~~ fun dict_cond_ord   : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order

"~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order

"~~~~~~~~~~~~~~~~~~~ fun get_basStr  : term -> string                       used twice --vv

"~~~~~~~~~~~~~~~~~~~ fun get_potStr  : term -> string                       used twice --vv

"~~~~~~~~~~~~~~~ fun monom_degree    : term list -> int

"~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order

"~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option

"~~~~~~~~~~~~~~~~~ fun koeff2ordStr  : term option -> string

"~~~~~ fun is_multUnordered

"~~~~~~~ fun sort_variables

"~~~~~~~~~ fun sort_varList

"~~~~~~~~~~~ fun var_ord

"~~~~~~~~~~~~~ fun get_basStr                                               used twice --^^

"~~~~~~~~~~~~~ fun get_potStr                                               used twice --^^

fun int_ord (i1, i2) =

(@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};

  Int.compare (i1, i2)

);

fun var_ord (a, b) = 

(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",

   sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

  prod_ord string_ord string_ord 

  ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

);

fun var_ord_revPow (a, b: term) = 

(@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",

    sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

  prod_ord string_ord string_ord_rev 

    ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

);

fun sort_varList ts =

(@{print} {a = "sort_varList", args = UnparseC.terms ts};

  sort var_ord ts

);

fun dict_cond_ord _ _ ([], [])     = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

  | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)

  | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)

  | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =

    (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")", 

      is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};

     case (cond x, cond y) of 

	    (false, false) =>

        (case elem_ord (x, y) of 

				  EQUAL => dict_cond_ord elem_ord cond (xs, ys) 

			  | ord => ord)

    | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)

    | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)

    | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys)

);

fun compare_koeff_ord (xs, ys) =

(@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",

    sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};

  string_ord

  ((koeff2ordStr o get_koeff_of_mon) xs,

   (koeff2ordStr o get_koeff_of_mon) ys)

);

fun var_ord (a,b: term) = 

(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",

   sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

  prod_ord string_ord string_ord 

  ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

);

*)

"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";

"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";

"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";

(* thus   ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.

  sym_real_mult_minus1                                  =     "- ?z = - 1 * ?z" *)

@{thm real_mult_minus1};                              (* = "- 1 * ?z = - ?z"     *)

val thm_isac = ThmC.sym_thm @{thm real_mult_minus1};  (* =     "- ?z = - 1 * ?z" *)

val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";

val SOME (t', []) = rewrite_ @{context} tless_true Rule_Set.empty true thm_isac t_isac;

if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("- 1", _)*))

else error "thm  - ?z = - 1 * ?z  loops with new numerals";

"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";

"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";

"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";

val thy = Proof_Context.init_global @{theory Partial_Fractions}

val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;

"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";

"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";

"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";

val t = TermC.parseNEW' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";

val SOME (id, t') = eval_is_expanded_in 0 0 t 0;

if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"

         andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"

then () else error "eval_is_expanded_in x ..changed";

val thy = Proof_Context.init_global @{theory Partial_Fractions}

val t = TermC.parseNEW' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";

val SOME (id, t') = eval_is_expanded_in 0 0 t 0;

if  UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"

          andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"

then () else error "eval_is_expanded_in AA ..changed";

val t = TermC.parseNEW' thy "(8 + 2*x + x \<up> 2) is_poly_in x";

val SOME (id, t') = eval_is_poly_in 0 0 t 0;

if  UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"

          andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"

then () else error "is_poly_in x ..changed";

val t = TermC.parseNEW' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";

val SOME (id, t') = eval_is_poly_in 0 0 t 0;

if  UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"

          andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"

then () else error "is_poly_in AA ..changed";

val thy = Proof_Context.init_global @{theory Partial_Fractions}

val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;

"-------- investigate (new 2002) uniary minus --------------------------------------------------";

"-------- investigate (new 2002) uniary minus --------------------------------------------------";

"-------- investigate (new 2002) uniary minus --------------------------------------------------";

val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)

TermC.atom_trace_detail @{context} t;

(*

*** Const (HOL.Trueprop, bool => prop)

*** . Const (HOL.eq, real => real => bool)

*** . . Const (Groups.minus_class.minus, real => real => real)

*** . . . Const (Groups.zero_class.zero, real)

*** . . . Var ((x, 0), real)

*** . . Const (Groups.uminus_class.uminus, real => real)

*** . . . Var ((x, 0), real)

*)

case t of

  Const (\<^const_name>\<open>Trueprop\<close>, _) $

    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ 

      (Const (\<^const_name>\<open>minus\<close>, _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _) $ 

        Var (("x", 0), _)) $

             (Const (\<^const_name>\<open>uminus\<close>, _) $ Var (("x", 0), _))) => ()

| _ => error "internal representation of \"0 - ?x = - ?x\" changed";

val t = TermC.parseNEW' thy "- 1";

TermC.atom_trace_detail @{context} t;

(*

*** 

*** Free (- 1, real)

*** 

*)

case t of

 Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) => ()

| _ => error "internal representation of \"- 1\" changed";

"======= these external values all have the same internal representation";

(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)

(*----------------------------------- vvvvv -------------------------------------------*)

val t = TermC.parseNEW' thy "-x";

TermC.atom_trace_detail @{context} t;

(**** -------------

*** Free ( -x, real)*)

case t of

  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()

| _ => error "internal representation of \"-x\" changed";

(*----------------------------------- vvvvv -------------------------------------------*)

val t = TermC.parseNEW' thy "- x";

TermC.atom_trace_detail @{context} t;

(**** -------------

*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)

case t of

  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()

| _ => error "internal representation of \"- x\" changed";

(*----------------------------------- vvvvvv ------------------------------------------*)

val t = TermC.parseNEW' thy "-(x)";

TermC.atom_trace_detail @{context} t;

(**** -------------

*** Free ( -x, real)*)

case t of

  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()

| _ => error "internal representation of \"-(x)\" changed";

"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";

"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";

"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";

(* indentation partially indicates call hierarchy:

"~~~~~ fun is_addUnordered

"~~~~~~~ fun is_polyexp

"~~~~~~~ fun sort_monoms

"~~~~~~~~~ fun sort_monList

"~~~~~~~~~~~ fun koeff_degree_ord

"~~~~~~~~~~~~~ fun degree_ord

"~~~~~~~~~~~~~~~ fun dict_cond_ord

"~~~~~~~~~~~~~~~~~ fun var_ord_revPow

"~~~~~~~~~~~~~~~~~~~ fun get_basStr         used twice --vv

"~~~~~~~~~~~~~~~~~~~ fun get_potStr         used twice --vv

"~~~~~~~~~~~~~~~ fun monom_degree

"~~~~~~~~~~~~~ fun compare_koeff_ord

"~~~~~~~~~~~~~~~ fun get_koeff_of_mon

"~~~~~~~~~~~~~~~~~ fun koeff2ordStr

"~~~~~ fun is_multUnordered

"~~~~~~~ fun sort_variables

"~~~~~~~~~ fun sort_varList

"~~~~~~~~~~~ fun var_ord

"~~~~~~~~~~~~~ fun get_basStr               used twice --^^

"~~~~~~~~~~~~~ fun get_potStr               used twice --^^

*)

val t = TermC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";

           eval_is_addUnordered "xxx" "yyy" t @{context};

"~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _, 

		       (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =

  ("xxx", "yyy", t, @{context});

    (*if*) is_addUnordered arg;

"~~~~~ fun is_addUnordered , args:"; val (t) = (arg);

  ((is_polyexp t) andalso not (t = sort_monoms t));

        (t = sort_monoms t);

"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);

  	val ll =  map monom2list (poly2list t);

  	val lls =

           sort_monList ll;

"~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);

      val xxx = 

            sort koeff_degree_ord ll(*return value*);

"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);

                 koeff_degree_ord: term list * term list -> order;

(*we check all elements at once..*)

val eee1 = ll |> nth 1;

val eee2 = ll |> nth 2;

val eee3 = ll |> nth 3;

val eee3 = ll |> nth 3;

val eee4 = ll |> nth 4;

if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";

if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";

if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";

if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";

if koeff_degree_ord (eee1, eee1) = EQUAL   then () else error "(eee1, eee1) CHANGED";

if koeff_degree_ord (eee1, eee2) = LESS    then () else error "(eee1, eee2) CHANGED";

if koeff_degree_ord (eee1, eee3) = LESS    then () else error "(eee1, eee3) CHANGED";

if koeff_degree_ord (eee1, eee4) = LESS    then () else error "(eee1, eee4) CHANGED";

if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";

if koeff_degree_ord (eee2, eee2) = EQUAL   then () else error "(eee2, eee4) CHANGED";

if koeff_degree_ord (eee2, eee3) = LESS    then () else error "(eee2, eee3) CHANGED";

if koeff_degree_ord (eee2, eee4) = LESS    then () else error "(eee2, eee4) CHANGED";

if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";

if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";

if koeff_degree_ord (eee3, eee3) = EQUAL   then () else error "(eee3, eee3) CHANGED";

if koeff_degree_ord (eee3, eee4) = LESS    then () else error "(eee3, eee4) CHANGED";

if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";

if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";

if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";

if koeff_degree_ord (eee4, eee4) = EQUAL   then () else error "(eee4, eee4) CHANGED";

"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();

                   degree_ord: term list * term list -> order;

if degree_ord (eee1, eee1) = EQUAL   then () else error "degree_ord (eee1, eee1) CHANGED";

if degree_ord (eee1, eee2) = LESS    then () else error "degree_ord (eee1, eee2) CHANGED";

if degree_ord (eee1, eee3) = LESS    then () else error "degree_ord (eee1, eee3) CHANGED";

if degree_ord (eee1, eee4) = LESS    then () else error "degree_ord (eee1, eee4) CHANGED";

if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";

if degree_ord (eee2, eee2) = EQUAL   then () else error "degree_ord (eee2, eee4) CHANGED";

if degree_ord (eee2, eee3) = EQUAL   then () else error "degree_ord (eee2, eee3) CHANGED";

if degree_ord (eee2, eee4) = LESS    then () else error "degree_ord (eee2, eee4) CHANGED";

if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";

if degree_ord (eee3, eee2) = EQUAL   then () else error "degree_ord (eee3, eee4) CHANGED";

if degree_ord (eee3, eee3) = EQUAL   then () else error "degree_ord (eee3, eee3) CHANGED";

if degree_ord (eee3, eee4) = LESS    then () else error "degree_ord (eee3, eee4) CHANGED";

if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";

if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";

if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";

if degree_ord (eee4, eee4) = EQUAL   then () else error "degree_ord (eee4, eee4) CHANGED";

"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();

dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;

dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;

dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;

val xxx = dict_cond_ord var_ord_revPow is_nums;

(* output from:

fun var_ord_revPow (a,b: term) =

 (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};

  @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

  prod_ord string_ord string_ord_rev 

    ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));

*)

if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";

if xxx (eee1, eee2) = LESS  then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";

if xxx (eee1, eee3) = LESS  then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";

if xxx (eee1, eee4) = LESS  then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";

(*-------------------------------------------------------------------------------------*)

if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";

if xxx (eee2, eee2) = EQUAL   then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";

if xxx (eee2, eee3) = EQUAL   then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";

if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";

(*-------------------------------------------------------------------------------------*)

if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";

if xxx (eee3, eee2) = EQUAL   then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";

if xxx (eee3, eee3) = EQUAL   then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";

if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";

(*-------------------------------------------------------------------------------------*)

if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";

if xxx (eee4, eee2) = LESS    then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";

if xxx (eee4, eee3) = LESS    then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";

if xxx (eee4, eee4) = EQUAL   then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";

(*-------------------------------------------------------------------------------------*)

"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();

(* we check all at once//*)

if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";

if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";

if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";

if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";

"~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();

                   compare_koeff_ord: term list * term list -> order;

(* we check all at once//*)

if compare_koeff_ord (eee1, eee1) = EQUAL   then () else error "_koeff_ord (eee1, eee1) CHANGED";

if compare_koeff_ord (eee1, eee2) = LESS    then () else error "_koeff_ord (eee1, eee2) CHANGED";

if compare_koeff_ord (eee1, eee3) = LESS    then () else error "_koeff_ord (eee1, eee3) CHANGED";

if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";

if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";

if compare_koeff_ord (eee2, eee2) = EQUAL   then () else error "_koeff_ord (eee2, eee2) CHANGED";

if compare_koeff_ord (eee2, eee3) = LESS    then () else error "_koeff_ord (eee2, eee3) CHANGED";

if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";

if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";

if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";

if compare_koeff_ord (eee3, eee3) = EQUAL   then () else error "_koeff_ord (eee3, eee3) CHANGED";

if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";

if compare_koeff_ord (eee4, eee1) = LESS    then () else error "_koeff_ord (eee4, eee1) CHANGED";

if compare_koeff_ord (eee4, eee2) = LESS    then () else error "_koeff_ord (eee4, eee2) CHANGED";

if compare_koeff_ord (eee4, eee3) = LESS    then () else error "_koeff_ord (eee4, eee3) CHANGED";

if compare_koeff_ord (eee4, eee4) = EQUAL   then () else error "_koeff_ord (eee4, eee4) CHANGED";

"~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();

           get_koeff_of_mon: term list -> term option;

val SOME xxx1 = get_koeff_of_mon eee1;

val SOME xxx2 = get_koeff_of_mon eee2;

val SOME xxx3 = get_koeff_of_mon eee3;

val NONE = get_koeff_of_mon eee4;

if UnparseC.term xxx1 = "1"   then () else error "get_koeff_of_mon eee1 CHANGED";

if UnparseC.term xxx2 = "2"   then () else error "get_koeff_of_mon eee2 CHANGED";

if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";

"~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();

                       koeff2ordStr: term option -> string;

if koeff2ordStr (SOME xxx1) = "1"   then () else error "koeff2ordStr eee1 CHANGED";

if koeff2ordStr (SOME xxx2) = "2"   then () else error "koeff2ordStr eee2 CHANGED";

if koeff2ordStr (SOME xxx3) = "40"  then () else error "koeff2ordStr eee3 CHANGED";

if koeff2ordStr NONE        = "---" then () else error "koeff2ordStr eee4 CHANGED";

"-------- examples from textbook Schalk I ------------------------------------------------------";

"-------- examples from textbook Schalk I ------------------------------------------------------";

"-------- examples from textbook Schalk I ------------------------------------------------------";

"-----SPB Schalk I p.63 No.267b ---";

val t = TermC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";

val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"

then () else error "poly.sml: diff.behav. in make_polynomial 1";

"-----SPB Schalk I p.63 No.275b ---";

val t = TermC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = 

  "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"

then () else error "poly.sml: diff.behav. in make_polynomial 2";

"-----SPB Schalk I p.63 No.279b ---";

val t = TermC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = 

  ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^

  "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^

  "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^

  " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")

then () else error "poly.sml: diff.behav. in make_polynomial 3";

(*associate poly*)

"-----SPB Schalk I p.63 No.291 ---";

val t = TermC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"

then () else error "poly.sml: diff.behav. in make_polynomial 4";

"-----SPB Schalk I p.64 No.295c ---";

val t = TermC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t =

  "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"

then ()else error "poly.sml: diff.behav. in make_polynomial 5";

"-----SPB Schalk I p.64 No.299a ---";

val t = TermC.parse_test @{context} "(x - y)*(x + y)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"

then () else error "poly.sml: diff.behav. in make_polynomial 6";

"-----SPB Schalk I p.64 No.300c ---";

val t = TermC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"

then () else error "poly.sml: diff.behav. in make_polynomial 7";

"-----SPB Schalk I p.64 No.302 ---";

val t = TermC.parse_test @{context}

  "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

if UnparseC.term t = "0"

then () else error "poly.sml: diff.behav. in make_polynomial 8";

(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)

"-----SPB Schalk I p.64 No.306a ---";

val t = TermC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()

else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";

(*WN071729 when reducing "rls reduce_012_" for Schaerding,

the above resulted in the term below ... but reduces from then correctly*)

val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"

then () else error "poly.sml: diff.behav. in make_polynomial 9b";

"-----SPB Schalk I p.64 No.296a ---";

val t = TermC.parse_test @{context} "(x - a) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

val NONE = eval_is_even "aaa" "bbb" (TermC.parse_test @{context} "3::real") "ccc";

if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 10";

"-----SPB Schalk I p.64 No.296c ---";

val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 11";

"-----SPB Schalk I p.62 No.242c ---";

val t = TermC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1"

then () else error "poly.sml: diff.behav. in make_polynomial 12";

"-----SPB Schalk I p.60 No.209a ---";

val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 7"

then () else error "poly.sml: diff.behav. in make_polynomial 13";

"-----SPB Schalk I p.60 No.209d ---";

val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "d \<up> 3"

then () else error "poly.sml: diff.behav. in make_polynomial 14";

"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";

"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";

"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";

"-----Schalk I p.64 No.303 ---";

val t = TermC.parse_test @{context} "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";

(*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)

val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "1280 * b \<up> 4"

then () else error "poly.sml: diff.behav. in make_polynomial 14b";

(* Richtig - aber Binomische Formel wurde nicht verwendet! *)

(*SOMETIMES LOOPS--------------------------------------------------------------------------//*)

"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";

"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";

"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";

"-----SPO ---";

val t = TermC.parse_test @{context} "a + a + a";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "3 * a" then ()

else error "poly.sml: diff.behav. in make_polynomial 16";

"-----SPO ---";

val t = TermC.parse_test @{context} "a + b + b + b";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a + 3 * b" then ()

else error "poly.sml: diff.behav. in make_polynomial 17";

"-----SPO ---";

val t = TermC.parse_test @{context} "b * a * a";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 2 * b" then ()

else error "poly.sml: diff.behav. in make_polynomial 21";

"-----SPO ---";

val t = TermC.parse_test @{context} "(a \<up> 2) \<up> 3";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "a \<up> 6" then ()

else error "poly.sml: diff.behav. in make_polynomial 22";

"-----SPO ---";

val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";

val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()

else error "poly.sml: diff.behav. in make_polynomial 23";

"-----SPO ---";

val t = TermC.parse_test @{context} "a * b * b \<up> (- 1) + a";

val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "2 * a" then ()

else error "poly.sml: diff.behav. in make_polynomial 25";

"-----SPO ---";

val t = TermC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";

val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;

if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"

then () else error "poly.sml: diff.behav. in make_polynomial 26";

(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)

"-----SPO ---";

val t = TermC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";

val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;

if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"

then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)

val t = TermC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";

val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;

if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"

then () else error "poly.sml: diff.behav. in make_polynomial 28";

"-------- check pbl  'polynomial simplification' -----------------------------------------------";

"-------- check pbl  'polynomial simplification' -----------------------------------------------";

"-------- check pbl  'polynomial simplification' -----------------------------------------------";

val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];

"-----0 ---";

case Refine.xxxxx @{context} fmz ["polynomial", "simplification"] of

    [M_Match.Matches (["polynomial", "simplification"], _)] => ()

  | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";

(*...if there is an error, then ...*)

"----- 1 ---";

(*default_print_depth 7;*)

val pbt = Problem.from_store @{context} ["polynomial", "simplification"];

(*default_print_depth 3;*)

(*if there is ...

> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;

... then Rewrite.trace_on:*)

"----- 2 ---";

M_Match.match_pbl fmz pbt;

(*... if there is no rewrite, then there is something wrong with where_rls*)

"-----3 ---";

(*default_print_depth 7;*)

val where_rls = (#where_rls o Problem.from_store @{context}) ["polynomial", "simplification"];

(*default_print_depth 3;*)

val t = TermC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";

val SOME (t',_) = rewrite_set_ thy false where_rls t;

if t' = @{term True} then () 

else error "poly.sml: diff.behav. in check pbl 'polynomial..";

(*... if this works, but -- 1-- does still NOT work, check types:*)

"-----4 ---";

(*show_types:=true;*)

(*

> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;

val wh = [False "(t_::real => real) (is_polyexp::real)"]

...................... \<up> \<up> \<up>  \<up> ............... \<up> ^*)

val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;

(*show_types:=false;*)

"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";

"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";

val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];

val (dI',pI',mI') =

  ("Poly",["polynomial", "simplification"],

   ["simplification", "for_polynomials"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n  (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)

(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =

(*+*)  "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n  (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"

(*+*)then () else error "No.267b: I_Model.T CHANGED";

( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)

(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"

(*+*)then () else error "";

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)

(*+*)if f2str f = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"

(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b - 1";

(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)

"-------- interSteps for Schalk 299a -----------------------------------------------------------";

"-------- interSteps for Schalk 299a -----------------------------------------------------------";

"-------- interSteps for Schalk 299a -----------------------------------------------------------";

States.reset ();

CalcTree @{context}

[(["Term ((x - y)*(x + (y::real)))", "normalform N"], 

  ("Poly",["polynomial", "simplification"],

  ["simplification", "for_polynomials"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);

val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

if existpt' ([1,1], Frm) pt then ()

else error "poly.sml: interSteps doesnt work again 1";

interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);

val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

(*============ inhibit exn WN120316 ==============================================

if existpt' ([1,1,1], Frm) pt then ()

else error "poly.sml: interSteps doesnt work again 2";

============ inhibit exn WN120316 ==============================================*)

"-------- ord_make_polynomial ------------------------------------------------------------------";

"-------- ord_make_polynomial ------------------------------------------------------------------";

"-------- ord_make_polynomial ------------------------------------------------------------------";

val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";

val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";

if ord_make_polynomial true @{context} [] (t1, t2) then ()

else error "poly.sml: diff.behav. in ord_make_polynomial";

(*SO: WHY IS THERE NO REWRITING ...*)

val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)";

(*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;

(* 

WHY IS THERE NO REWRITING ?!?

most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,

while order_add_mult uses isac's rewriter -- and this is used rarely!

*)