(* Knowledge/poly.sml

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

"-------- fun is_polyexp -----------------------------------------------------------------------";

"-------- fun has_degree_in --------------------------------------------------------------------";

"-------- fun mono_deg_in ----------------------------------------------------------------------";

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

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

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

"-------- fun sort_variables -------------------------------------------------------------------";

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

"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";

"-------- check make_polynomial with simple terms ----------------------------------------------";

"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";

"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";

"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";

"-------- fun is_multUnordered  b * a * a ------------------------------------------------------";

"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";

"-------- 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_ @{theory} 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";

"-------- fun is_polyexp -----------------------------------------------------------------------";

"-------- fun is_polyexp -----------------------------------------------------------------------";

"-------- fun is_polyexp -----------------------------------------------------------------------";

val t = TermC.str2term "x / x";

if is_polyexp t then error "NOT is_polyexp (x / x)" else ();

val t = TermC.str2term "-1 * A * 3";

if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";

val t = TermC.str2term "-1 * AA * 3";

if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";

val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";

if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";

"-------- fun has_degree_in --------------------------------------------------------------------";

"-------- fun has_degree_in --------------------------------------------------------------------";

"-------- fun has_degree_in --------------------------------------------------------------------";

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "1";

if has_degree_in t v = 0 then () else error "has_degree_in (1) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "1";

if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";

if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";

if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";

if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";

if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";

if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "x";

if has_degree_in t v = 1 then () else error "has_degree_in (x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA";

if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";

if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";

if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";

"-------- fun mono_deg_in ----------------------------------------------------------------------";

"-------- fun mono_deg_in ----------------------------------------------------------------------";

"-------- fun mono_deg_in ----------------------------------------------------------------------";

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";

if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "x";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";

if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";

if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";

(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)

val thy = @{theory Partial_Fractions}

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";

if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";

if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA";

if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";

if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";

if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";

"-------- 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 = @{theory Partial_Fractions}

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const ("HOL.True", _), []) = 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 = (Thm.term_of o the o (TermC.parse 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 = @{theory Partial_Fractions}

val t = (Thm.term_of o the o (TermC.parse 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 = (Thm.term_of o the o (TermC.parse 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 = (Thm.term_of o the o (TermC.parse 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 = @{theory Partial_Fractions}

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;

val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";

val SOME (Const ("HOL.True", _), []) = 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.atomty 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 ("HOL.Trueprop", _) $

    (Const ("HOL.eq", _) $ 

      (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $ 

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

             (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()

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

val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";

TermC.atomty t;

(*

*** 

*** Free (-1, real)

*** 

*)

case t of

 Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()

| _ => 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 = (Thm.term_of o the o (TermC.parse thy)) "-x";

TermC.atomty t;

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

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

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

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

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

val t = (Thm.term_of o the o (TermC.parse thy)) "- x";

TermC.atomty t;

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

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

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

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

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

val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";

TermC.atomty t;

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

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

case t of

  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

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

"-------- fun sort_variables -------------------------------------------------------------------";

"-------- fun sort_variables -------------------------------------------------------------------";

"-------- fun sort_variables -------------------------------------------------------------------";

if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()

else error "lexicographic order CHANGED";

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

val t =  @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)

val t' =  sort_variables t;

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

else error "sort_variables  3 * b + a * 2  CHANGED";

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

  	val ll =  map monom2list (poly2list t);

(*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";

(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],

(*+*)      [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]

(*+*)    ] = map monom2list (poly2list t);

  	val lls = map sort_varList ll;

(*+*)case map sort_varList ll of

(*+*)  [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],

(*+*)    [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]

(*+*)  ] => ()

(*+*)| _ => error "map sort_varList CHANGED";

  	val T = type_of t;

  	val ls = map (create_monom T) lls;

(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),

(*+*)     Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;

(*+*)case map (create_monom T) lls of

(*+*)  [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),

(*+*)   Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)

(*+*)  ] => ()

(*+*)| _ => error "map (create_monom T) CHANGED";

  val xxx = (*in*) create_polynom T ls (*end*);

(*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()

(*+*)else error "create_polynom CHANGED";

(* done by rewriting>              2 * a +       3 * b ? *)

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

val t =  @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)

val t' =     sort_variables t;

if UnparseC.term t' = "3 * a + - 2 * a" then ()

else error "sort_variables  3 * a + - 2 * a  CHANGED";

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

  	val ll =  map monom2list (poly2list t);

(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],

(*+*)      [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)

(*+*)    ] = map monom2list (poly2list t);

  	val lls = map

           sort_varList ll;

(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],

(*+*)      [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)

(*+*)    ] = map sort_varList ll;

       map sort_varList ll;

"~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);

val sorted = sort var_ord ts;

(*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"

(*+*)then () else error "sort var_ord  [\"- 2\", \"a\"]  CHANGED";

(*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"

(*+*)then () else error "get_basStr  - 2  CHANGED";

(*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"

(*+*)then () else error "get_basStr  a  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.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";

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

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

		       (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =

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

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

"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";

"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";

"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";

val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";

Rewrite.trace_on := false;

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

   UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";

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

(** )

##  rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y 

###  rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y 

######  rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered 

#######  try calc: "Poly.is_addUnordered" 

########  eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False"  (*isa*)

                                                                              True"   (*isa2*)

#######  calc. to: False  (*isa*)

                   True   (*isa2*)

( **)

        if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()

else error"is_addUnordered  x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)

"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");

      ((is_polyexp t) andalso not (t = sort_monoms t)) = false;  (*isa == isa2*)

(*+*) if is_polyexp t = true then () else error "is_polyexp  x \<up> 2 * y \<up> 2 + x \<up> 3 * y";

(*+*) if                           t = sort_monoms t = false then () else error "sort_monoms 123";

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

  	val ll =  map monom2list (poly2list t);

  	val lls = sort_monList ll;

(*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)

(*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)

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

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

val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";

val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";    

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

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

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

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

(* isa -- isa2:

(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"}                                           (*isa == isa2*)

(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"}                                            (*isa == isa2*)

(*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*) 

(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"}                                           (*isa == isa2*) 

(*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"}                                           (*isa == isa2*) 

(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"}                                           (*isa == isa2*)

(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"}                                                       (*isa == isa2*)

(*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"}                (*isa == isa2*) 

val it = true: bool

val it = true: bool

val it = true: bool

val it = true: bool*)

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

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

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

(*{a = "int_ord (4, 10003) = ", z = LESS}      isa

  {a = "int_ord (4, 4) = ", z = EQUAL}         isa2*)

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

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

(* isa -- isa2:

(*1*){a = "int_ord (10002, 10002) = ", z = EQUAL}                                                          (*isa*)

     {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)

(*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}  (*isa*)

(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"}               (*isa*)

(*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"}        (*isa*)

(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"}               (*isa*)

(*1*){a = "dict_cond_ord ([], [])"}                                                                        (*isa*)

(*2*){a = "int_ord (10002, 10003) = ", z = LESS}                                                           (*isa*)

     {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)

     {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)

(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"}                 (*isa2*)

(*3*){a = "int_ord (10003, 10002) = ", z = GREATER}                                                       (*isa*)

     {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)

     {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}

(*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"}                (*isa == isa2*)

(*4*){a = "int_ord (10003, 10003) = ", z = EQUAL}                                                         (*isa*)

     {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)

(*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)

(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"}              (*isa == isa2*)

(*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"}                       (*isa == isa2*)

(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"}                          (*isa == isa2*)

(*4*){a = "dict_cond_ord ([], [])"}                                                                       (*isa == isa2*)

val it = true: bool

val it = false: bool

val it = false: bool

val it = true: bool

*)

(*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";

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

"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )

	    (*if*) (is_nums x) (*else*);

  val (Const ("Transcendental.powr", _) $ Free _ $ t) =

      (*case*) x (*of*); 

(*+*)UnparseC.term x = "x \<up> 2";

            (*if*) TermC.is_num t (*then*);

           counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);

"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);

	    (*if*) (is_nums x) (*else*);

  val (Const ("Transcendental.powr", _) $ Free _ $ t) =

      (*case*) x (*of*); 

(*+*)UnparseC.term x = "y \<up> 2";

            (*if*) TermC.is_num t (*then*);

  val return =

      counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);

if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";

( *---------------------------------------------------------------------------------OPEN local/*)

(*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()

else error "monom_degree  [\"x \<up> 3\", \"y\"] CHANGED";

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

"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )

	    (*if*) (is_nums x) (*else*);

val (Const ("Transcendental.powr", _) $ Free _ $ t) =

      (*case*) x (*of*); 

(*+*)UnparseC.term x = "x \<up> 3";

            (*if*) TermC.is_num t (*then*);

      counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);

"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);

	    (*if*) (is_nums x) (*else*);

val _ = (*the default case*)

      (*case*) x (*of*); 

( *---------------------------------------------------------------------------------OPEN local/*)

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

val xxx = dict_cond_ord var_ord_revPow is_nums;

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

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

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

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

"-------- check make_polynomial with simple terms ----------------------------------------------";

"-------- check make_polynomial with simple terms ----------------------------------------------";

"-------- check make_polynomial with simple terms ----------------------------------------------";

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

val t = TermC.str2term "2*3*a";

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

if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";

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

val t = TermC.str2term "2*a + 3*a";

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

if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";

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

val t = TermC.str2term "2*a + 3*a + 3*a";

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

if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";

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

val t = TermC.str2term "3*a - 2*a";

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

if UnparseC.term t = "a" then () else error "check make_polynomial 4";

"----- check 5 ---";

val t = TermC.str2term "4*(3*a - 2*a)";

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

if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";

"----- check 6 ---";

val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";

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

if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";

"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";

"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";

"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";

val thy = @{theory "Isac_Knowledge"};

"===== works for a simple example, see rewrite.sml -- fun app_rev ===";

val t = TermC.str2term "x \<up> 2 * x";

val SOME (t', _) = rewrite_set_ thy true order_mult_ t;

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

else error "poly.sml Poly.is_multUnordered doesn't work";

(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:

###  rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +

 (-48 * x \<up> 4 + 8))

######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered

#######  try calc: Poly.is_multUnordered'

=======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!

*)

val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))";

"----- is_multUnordered ---";

val tsort = sort_variables t;

UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n-1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n-1 * (-1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";

is_polyexp t;

tsort = t;

is_polyexp t andalso not (t = sort_variables t);

if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";

"----- eval_is_multUnordered ---";

val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";

case eval_is_multUnordered "testid" "" tm thy of

    SOME (_, Const ("HOL.Trueprop", _) $ 

                   (Const ("HOL.eq", _) $

                          (Const ("Poly.is_multUnordered", _) $ _) $ 

                          Const ("HOL.True", _))) => ()

  | _ => error "poly.sml diff. eval_is_multUnordered";

"----- rewrite_set_ STILL DIDN'T WORK";

val SOME (t, _) = rewrite_set_ thy true order_mult_ t;

UnparseC.term t;

"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";

"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";

"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";

val thy = @{theory "Isac_Knowledge"};

val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";

(*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true

(*+*)  andalso not (is_multUnordered arg)

(*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";

case eval_is_multUnordered "xxx " "yyy " t thy of

  SOME

    ("xxx 3 * a + - 2 * a_",

      Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $

        Const ("HOL.False", _))) => ()

(*      Const ("HOL.True", _))) => ()   <<<<<--------------------------- this is false*)

| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";

"----- is_multUnordered --- (- 2 * a) is_multUnordered = False";

val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";

(*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true

(*+*)  andalso not (is_multUnordered arg)

(*+*)then () else error "sort_variables  - 2 * a   CHANGED";

case eval_is_multUnordered "xxx " "yyy " t thy of

  SOME

    ("xxx - 2 * a_",

      Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $

        Const ("HOL.False", _))) => ()

| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";

"----- is_multUnordered --- (a) is_multUnordered = False";

val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";

(*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true

(*+*)  andalso not (is_multUnordered arg)

(*+*)then () else error "sort_variables   a   CHANGED";

case eval_is_multUnordered "xxx " "yyy " t thy of

  SOME

    ("xxx a_",

      Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $

        Const ("HOL.False", _))) => ()

| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";

"----- is_multUnordered --- (- 2) is_multUnordered = False";

val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";

(*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true

(*+*)  andalso not (is_multUnordered arg)

(*+*)then () else error "sort_variables   - 2   CHANGED";

case eval_is_multUnordered "xxx " "yyy " t thy of

  SOME

    ("xxx - 2_",

      Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $

        Const ("HOL.False", _))) => ()

| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";

"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";

"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";

"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";

(*  ca.line 45 of Rewrite.trace_on:

##  rls: order_mult_rls_ on: 

  x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 

###  rls: order_mult_ on:

  x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 

######  rls: Rule_Set.empty-is_multUnordered on: 

  x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered 

#######  try calc: "Poly.is_multUnordered" 

########  eval asms: 

N:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered = True" 

-------------------------------------------------------------------------------------------------==

O:x \<up> 3 + 3 * x \<up> 2 * (-1 * a)  + 3 * x * (-1    \<up> 2 * a \<up> 2) + -1    \<up> 3 * a \<up> 3 is_multUnordered = True" 

#######  calc. to: True 

#######  try calc: "Poly.is_multUnordered" 

#######  try calc: "Poly.is_multUnordered" 

###  rls: order_mult_ on: 

N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2))  +  3 * (a \<up> 2 * (x * (- 1) \<up> 2))  +  a \<up> 3 * (- 1) \<up> 3 

--------+--------------------------+---------------------------------+---------------------------<>

O:x \<up> 3 + -1  * (3 * (a * x \<up> 2))  +  -1 \<up> 2 * (3 * (a \<up> 2 * x))     +  -1 \<up> 3 * a \<up> 3 

-------------------------------------------------------------------------------------------------<>

*)

val t = TermC.str2term "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3";

(*

"~~~~~ fun is_multUnordered

"~~~~~~~ fun sort_variables

"~~~~~~~~~ val sort_varList

*)

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

     is_polyexp t = true;

  val return =

             sort_variables t;

(*+*)if UnparseC.term return =

(*+*)  "x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) +\n(- 1) \<up> 2 * (3 * (a \<up> 2 * x)) +\n(- 1) \<up> 3 * a \<up> 3"

(*+*)then () else error "sort_variables  x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";

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

  	val ll = map monom2list (poly2list t);

  	val lls = map sort_varList ll; 

(*+*)val ori3 = nth 3 ll;

(*+*)val mon3 = nth 3 lls;

(*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";

(*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";

(*+*)if UnparseC.terms ori3       = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";

(*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";

(*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";