(* Title: test/Tools/isac/Knowledge/poly-1.sml

   Author: Walther Neuper

   Use is subject to license terms.

Test of basic functions and application to complex examples.

*)

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

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

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

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

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

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

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

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

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

"-------- norm_Poly with AlgEin ----------------------------------------------------------------";

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

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

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

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

"-------- 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 (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)

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

"-------- 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 (\<^const_name>\<open>numeral\<close>, _) $ _), Free ("b", _)],

(*+*)      [Free ("a", _), (Const (\<^const_name>\<open>numeral\<close>, _) $ _)]

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

  	val lls = map sort_varList ll;

(*+*)case map sort_varList ll of

(*+*)  [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("b", _)],

(*+*)    [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)]

(*+*)  ] => ()

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

  	val T = type_of t;

  	val ls = map (create_monom T) lls;

(*+*)val [Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("b", _),

(*+*)     Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("a", _)] = map (create_monom T) lls;

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

(*+*)  [Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("b", _),

(*+*)   Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ 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 (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],

(*+*)      [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*already correct order*)

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

  	val lls = map

           sort_varList ll;

(*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],

(*+*)      [Const (\<^const_name>\<open>uminus\<close>, _) $ _, 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";

"-------- 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; (*true 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 (\<^const_name>\<open>powr\<close>, _) $ 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 (\<^const_name>\<open>powr\<close>, _) $ 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 (\<^const_name>\<open>powr\<close>, _) $ 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 (\<^const_name>\<open>Trueprop\<close>, _) $ 

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

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

                          Const (\<^const_name>\<open>True\<close>, _))) => ()

  | _ => 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 (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $

        Const (\<^const_name>\<open>False\<close>, _))) => ()

(*      Const (\<^const_name>\<open>True\<close>, _))) => ()   <<<<<--------------------------- 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 (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $

        Const (\<^const_name>\<open>False\<close>, _))) => ()

| _ => 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 (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $

        Const (\<^const_name>\<open>False\<close>, _))) => ()

| _ => 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 (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $

        Const (\<^const_name>\<open>False\<close>, _))) => ()

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

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

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

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

"~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);

(* Output below with:

val sort_varList = sort var_ord;

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))

);

*)

(*+*)val xxx = sort_varList ori3;

(*

{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)

{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)

isa                                            isa2

{a = "var_ord ", a_b = "(3, x)"}               {a = "var_ord ", a_b = "(3, x)"}

  {sort_args = "(|||, ||||||), (x, ---)"}        {sort_args = "(|||, ||||||), (x, ---)"}

{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}

  {sort_args = "(x, ---), (|||, ||||||)"}        {sort_args = "(x, ---), (|||, ||||||)"}

{a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}   {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}

  {sort_args = "(|||, ||||||), (a, 2)"}          {sort_args = "(|||, ||||||), (a, |||)"}

                                  ^^^                                             ^^^

{a = "var_ord ", a_b = "(x, a \<up> 2)"}           {a = "var_ord ", a_b = "(x, a \<up> 2)"}

  {sort_args = "(x, ---), (a, 2)"}               {sort_args = "(x, ---), (a, |||)"}

                             ^^^                                             ^^^

{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}

  {sort_args = "(x, ---), (|||, ||||||)"}        {sort_args = "(x, ---), (|||, ||||||)"}

{a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}

  {sort_args = "(|||, ||||||), (|||, ||||||)"}   {sort_args = "(|||, ||||||), (|||, ||||||)"}

*)

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

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

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

val t = TermC.str2term "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";

"~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});

    ((is_polyexp t) andalso not (t = sort_variables t)) = true;  (*isa == isa2*)

(*+*)if    is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";

"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (t);

    (*if*) TermC.is_num num (*else*);

"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (num);

    (*if*) TermC.is_num num (*else*);

      (*if*) TermC.is_variable num (*then*);

                           val xxx = sort_variables t;

(*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";

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

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

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

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 "rewrite_set_ 2*3*a CHANGED";

(*

##  try calc: "Groups.times_class.times" 

##  rls: order_mult_rls_ on: 6 * a 

###  rls: order_mult_ on: 6 * a 

######  rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered 

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

########  eval asms: "6 * a is_multUnordered = True"    (*isa*)

                                             = False"   (*isa2*)

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

                   False (*isa2*)

*)

val t = TermC.str2term "(6 * a) is_multUnordered"; 

val SOME

    (_, t') =

           eval_is_multUnordered "xxx" () t @{theory};

(*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () 

(*+*)else error "6 * a is_multUnordered = False CHANGED";

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

		       (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory});

    (*if*) is_multUnordered arg (*else*);

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

  val return =

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

(*+*)return = false;                                             (*isa*)

(*+*)  is_polyexp t = true;                                      (*isa*)

(*+*)                        not (t = sort_variables t) = false; (*isa*)

                            val xxx = sort_variables t;

(*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";

"-------- norm_Poly with AlgEin ----------------------------------------------------------------";

"-------- norm_Poly with AlgEin ----------------------------------------------------------------";

"-------- norm_Poly with AlgEin ----------------------------------------------------------------";

val thy = @{theory AlgEin};

val SOME (f',_) = rewrite_set_ thy false norm_Poly

(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");

if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"

then ((*norm_Poly NOT COMPLETE -- TODO MG*))

else error "norm_Poly changed behavior";

(* isa:

##  rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben 

###  rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben 

######  rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +

oben is_addUnordered 

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

########  eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +

oben is_addUnordered = True" 

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

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

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

###  rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben 

*)

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

  (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");

(*+*)val t' =

           sort_monoms t;

(*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)

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

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

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

val t = TermC.str2term "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.str2term "(x - a) \<up> 3";

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

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.str2term "(-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.str2term "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.str2term "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.str2term "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";

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

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

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

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

val t = TermC.str2term "a \<up> 2*a \<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 15";

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

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

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

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

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

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

val t = TermC.str2term "a \<up> 2*a \<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 19";

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

val t = TermC.str2term "b + a - b";

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

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

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

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

val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";

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

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

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