walther@60328: (* Title: test/Tools/isac/Knowledge/poly-1.sml
walther@60328:    Author: Walther Neuper
walther@60328:    Use is subject to license terms.
walther@60328: 
walther@60328: Test of basic functions and application to complex examples.
walther@60328: *)
walther@60328: 
walther@60328: "-----------------------------------------------------------------------------------------------";
walther@60328: "-----------------------------------------------------------------------------------------------";
walther@60328: "table of contents -----------------------------------------------------------------------------";
walther@60328: "-----------------------------------------------------------------------------------------------";
walther@60328: "-------- fun is_polyexp -----------------------------------------------------------------------";
walther@60328: "-------- fun has_degree_in --------------------------------------------------------------------";
walther@60328: "-------- fun mono_deg_in ----------------------------------------------------------------------";
walther@60328: "-------- fun sort_variables -------------------------------------------------------------------";
walther@60328: "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
walther@60328: "-------- check make_polynomial with simple terms ----------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
walther@60328: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
walther@60328: "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
walther@60328: "-------- complex examples from textbook Schalk I ----------------------------------------------";
walther@60328: "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
walther@60328: "-----------------------------------------------------------------------------------------------";
walther@60328: "-----------------------------------------------------------------------------------------------";
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_polyexp -----------------------------------------------------------------------";
walther@60328: "-------- fun is_polyexp -----------------------------------------------------------------------";
walther@60328: "-------- fun is_polyexp -----------------------------------------------------------------------";
walther@60328: val t = TermC.str2term "x / x";
walther@60328: if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
walther@60328: 
walther@60329: val t = TermC.str2term "- 1 * A * 3";
walther@60329: if is_polyexp t then () else error "is_polyexp (- 1 * A * 3)";
walther@60328: 
walther@60329: val t = TermC.str2term "- 1 * AA * 3";
walther@60329: if is_polyexp t then () else error "is_polyexp (- 1 * AA * 3)";
walther@60328: 
walther@60328: val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
walther@60328: if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
walther@60328: 
walther@60328: "-------- fun has_degree_in --------------------------------------------------------------------";
walther@60328: "-------- fun has_degree_in --------------------------------------------------------------------";
walther@60328: "-------- fun has_degree_in --------------------------------------------------------------------";
Walther@60424: val thy = @{theory}
Walther@60424: val ctxt = Proof_Context.init_global thy
Walther@60424: val v = TermC.parseNEW' ctxt "x";
Walther@60424: val t = TermC.parseNEW' ctxt "1";
walther@60328: if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "1";
walther@60328: if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x";
Walther@60424: val t = TermC.parseNEW' ctxt "a*b+c";
walther@60328: if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "a*b+c";
walther@60328: if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x";
Walther@60424: val t = TermC.parseNEW' ctxt "a*x+c";
walther@60328: if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "a*AA+c";
walther@60328: if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
Walther@60424: val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";
walther@60328: if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
walther@60328: if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
Walther@60424: val t = TermC.parseNEW' ctxt "x \<up> 7";
walther@60328: if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "AA \<up> 7";
walther@60328: if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+x)*x";
walther@60328: if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
walther@60328: if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x";
Walther@60424: val t = TermC.parseNEW' ctxt "x";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "AA";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
walther@60328: 
walther@60328: (*----------*)
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
Walther@60424: val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
walther@60328: 
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
Walther@60424: val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
walther@60328: if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
walther@60328: 
walther@60328: "-------- fun mono_deg_in ----------------------------------------------------------------------";
walther@60328: "-------- fun mono_deg_in ----------------------------------------------------------------------";
walther@60328: "-------- fun mono_deg_in ----------------------------------------------------------------------";
Walther@60424: val v = TermC.parseNEW' ctxt "x::real";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
walther@60328: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";
walther@60328: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
walther@60328: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+x)*x";
walther@60328: if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "x::real";
walther@60328: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)";
walther@60328: if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
walther@60328: if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
walther@60328: 
walther@60336: (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
walther@60328: val thy = @{theory Partial_Fractions}
Walther@60424: val ctxt = Proof_Context.init_global thy
Walther@60424: val v = TermC.parseNEW' ctxt "AA";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
walther@60328: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "AA \<up> 7";
walther@60328: if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
walther@60328: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
walther@60328: if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "AA";
walther@60328: if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "(a*b+c)";
walther@60328: if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
walther@60328: 
Walther@60424: val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
walther@60328: if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
walther@60328: 
walther@60328: 
walther@60328: "-------- fun sort_variables -------------------------------------------------------------------";
walther@60328: "-------- fun sort_variables -------------------------------------------------------------------";
walther@60328: "-------- fun sort_variables -------------------------------------------------------------------";
walther@60328: if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
walther@60328: else error "lexicographic order CHANGED";
walther@60328: 
walther@60328: (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
walther@60328: val t =  @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
walther@60328: val t' =  sort_variables t;
walther@60328: if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
walther@60328: else error "sort_variables  3 * b + a * 2  CHANGED";
walther@60328: 
walther@60328: "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
walther@60328:   	val ll =  map monom2list (poly2list t);
walther@60328: 
walther@60328: (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
walther@60336: (*+*)val [ [(Const (\<^const_name>\<open>numeral\<close>, _) $ _), Free ("b", _)],
walther@60336: (*+*)      [Free ("a", _), (Const (\<^const_name>\<open>numeral\<close>, _) $ _)]
walther@60328: (*+*)    ] = map monom2list (poly2list t);
walther@60328: 
walther@60328:   	val lls = map sort_varList ll;
walther@60328: 
walther@60328: (*+*)case map sort_varList ll of
walther@60336: (*+*)  [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("b", _)],
walther@60336: (*+*)    [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)]
walther@60328: (*+*)  ] => ()
walther@60328: (*+*)| _ => error "map sort_varList CHANGED";
walther@60328: 
walther@60328:   	val T = type_of t;
walther@60328:   	val ls = map (create_monom T) lls;
walther@60328: 
walther@60336: (*+*)val [Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("b", _),
walther@60336: (*+*)     Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
walther@60328: 
walther@60328: (*+*)case map (create_monom T) lls of
walther@60336: (*+*)  [Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("b", _),
walther@60336: (*+*)   Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("a", _)
walther@60328: (*+*)  ] => ()
walther@60328: (*+*)| _ => error "map (create_monom T) CHANGED";
walther@60328: 
walther@60328:   val xxx = (*in*) create_polynom T ls (*end*);
walther@60328: 
walther@60328: (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
walther@60328: (*+*)else error "create_polynom CHANGED";
walther@60328: (* done by rewriting>              2 * a +       3 * b ? *)
walther@60328: 
walther@60328: (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
walther@60328: val t =  @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
walther@60328: val t' =     sort_variables t;
walther@60328: if UnparseC.term t' = "3 * a + - 2 * a" then ()
walther@60328: else error "sort_variables  3 * a + - 2 * a  CHANGED";
walther@60328: 
walther@60328: "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
walther@60328:   	val ll =  map monom2list (poly2list t);
walther@60328: 
walther@60336: (*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
walther@60336: (*+*)      [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*already correct order*)
walther@60328: (*+*)    ] = map monom2list (poly2list t);
walther@60328: 
walther@60328:   	val lls = map
walther@60328:            sort_varList ll;
walther@60328: 
walther@60336: (*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
walther@60336: (*+*)      [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
walther@60328: (*+*)    ] = map sort_varList ll;
walther@60328: 
walther@60328:        map sort_varList ll;
walther@60328: "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
walther@60328: val sorted = sort var_ord ts;
walther@60328: 
walther@60328: (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
walther@60328: (*+*)then () else error "sort var_ord  [\"- 2\", \"a\"]  CHANGED";
walther@60328: 
walther@60328: 
walther@60328: (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
walther@60328: (*+*)then () else error "get_basStr  - 2  CHANGED";
walther@60328: (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
walther@60328: (*+*)then () else error "get_basStr  a  CHANGED";
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
walther@60328: "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
walther@60328: "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
Walther@60500: val ctxt = Proof_Context.init_global @{theory}
walther@60328: val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328:    UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
walther@60328: if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 23";
walther@60328: 
walther@60328: (** )
walther@60328: ##  rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y 
walther@60328: ###  rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y 
walther@60328: ######  rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered 
walther@60328: #######  try calc: "Poly.is_addUnordered" 
walther@60328: ########  eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False"  (*isa*)
walther@60328:                                                                               True"   (*isa2*)
walther@60328: #######  calc. to: False  (*isa*)
walther@60328:                    True   (*isa2*)
walther@60328: ( **)
walther@60328:         if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
walther@60328: else error"is_addUnordered  x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
walther@60328: "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
walther@60328:       ((is_polyexp t) andalso not (t = sort_monoms t)) = false;  (*isa == isa2*)
walther@60328: 
walther@60328: (*+*) if is_polyexp t = true then () else error "is_polyexp  x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
walther@60328: 
walther@60328: (*+*) if                           t = sort_monoms t = false then () else error "sort_monoms 123";
walther@60328: "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
walther@60328:   	val ll =  map monom2list (poly2list t);
walther@60328:   	val lls = sort_monList ll;
walther@60328: 
walther@60328: (*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
walther@60328: (*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
walther@60328: 
walther@60328: "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
walther@60328: (* we check all elements at once..*)
walther@60328: val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
walther@60328: val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";    
walther@60328: 
walther@60328: (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL   then () else error "(eee1, eee1) CHANGED";
walther@60328: (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
walther@60328: (*3*)if koeff_degree_ord (eee2, eee1) = LESS    then () else error "(eee2, eee1) CHANGED"; (*isa*)
walther@60328: (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL   then () else error "(eee2, eee2) CHANGED";
walther@60328: (* isa -- isa2:
walther@60328: (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"}                                           (*isa == isa2*)
walther@60328: (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"}                                            (*isa == isa2*)
walther@60328: (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*) 
walther@60328: 
walther@60328: (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"}                                           (*isa == isa2*) 
walther@60328: 
walther@60328: (*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"}                                           (*isa == isa2*) 
walther@60328: 
walther@60328: (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"}                                           (*isa == isa2*)
walther@60328: (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"}                                                       (*isa == isa2*)
walther@60328: (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"}                (*isa == isa2*) 
walther@60328: val it = true: bool
walther@60328: val it = true: bool
walther@60328: val it = true: bool
walther@60328: val it = true: bool*)
walther@60328: 
walther@60328: "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
walther@60328: (*1*)if degree_ord (eee1, eee1) = EQUAL   then () else error "degree_ord (eee1, eee1) CHANGED";
walther@60328: (*2*)if degree_ord (eee1, eee2) = GREATER    then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
walther@60328: (*{a = "int_ord (4, 10003) = ", z = LESS}      isa
walther@60328:   {a = "int_ord (4, 4) = ", z = EQUAL}         isa2*)
walther@60328: (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
walther@60328: (*4*)if degree_ord (eee2, eee2) = EQUAL   then () else error "degree_ord (eee2, eee2) CHANGED";
walther@60328: (* isa -- isa2:
walther@60328: (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL}                                                          (*isa*)
walther@60328:      {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)
walther@60328: (*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}  (*isa*)
walther@60328: (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"}               (*isa*)
walther@60328: (*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"}        (*isa*)
walther@60328: (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"}               (*isa*)
walther@60328: (*1*){a = "dict_cond_ord ([], [])"}                                                                        (*isa*)
walther@60328: 
walther@60328: (*2*){a = "int_ord (10002, 10003) = ", z = LESS}                                                           (*isa*)
walther@60328:      {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)
walther@60328:      {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
walther@60328: (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"}                 (*isa2*)
walther@60328: 
walther@60328: (*3*){a = "int_ord (10003, 10002) = ", z = GREATER}                                                       (*isa*)
walther@60328:      {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)
walther@60328:      {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
walther@60328: (*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"}                (*isa == isa2*)
walther@60328: 
walther@60328: (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL}                                                         (*isa*)
walther@60328:      {a = "int_ord (4, 4) = ", z = EQUAL}                                                                    (*isa2*)
walther@60328: (*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
walther@60328: (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"}              (*isa == isa2*)
walther@60328: (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"}                       (*isa == isa2*)
walther@60328: (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"}                          (*isa == isa2*)
walther@60328: (*4*){a = "dict_cond_ord ([], [])"}                                                                       (*isa == isa2*)
walther@60328: 
walther@60328: val it = true: bool
walther@60328: val it = false: bool
walther@60328: val it = false: bool
walther@60328: val it = true: bool
walther@60328: *)
walther@60328: 
walther@60328: (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
walther@60328: "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
walther@60328: "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
walther@60328: 	    (*if*) (is_nums x) (*else*);
wenzelm@60405:   val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
walther@60328:       (*case*) x (*of*); 
walther@60328: (*+*)UnparseC.term x = "x \<up> 2";
walther@60328:             (*if*) TermC.is_num t (*then*);
walther@60328: 
walther@60328:            counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
walther@60328: "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
walther@60328: 	    (*if*) (is_nums x) (*else*);
wenzelm@60405:   val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
walther@60328:       (*case*) x (*of*); 
walther@60328: (*+*)UnparseC.term x = "y \<up> 2";
walther@60328:             (*if*) TermC.is_num t (*then*);
walther@60328: 
walther@60328:   val return =
walther@60328:       counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
walther@60328: if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
walther@60328: ( *---------------------------------------------------------------------------------OPEN local/*)
walther@60328: 
walther@60328: (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
walther@60328: else error "monom_degree  [\"x \<up> 3\", \"y\"] CHANGED";
walther@60328: "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
walther@60328: "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
walther@60328: 	    (*if*) (is_nums x) (*else*);
wenzelm@60405: val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
walther@60328:       (*case*) x (*of*); 
walther@60328: (*+*)UnparseC.term x = "x \<up> 3";
walther@60328:             (*if*) TermC.is_num t (*then*);
walther@60328: 
walther@60328:       counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
walther@60328: "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
walther@60328: 	    (*if*) (is_nums x) (*else*);
walther@60328: val _ = (*the default case*)
walther@60328:       (*case*) x (*of*); 
walther@60328: ( *---------------------------------------------------------------------------------OPEN local/*)
walther@60328: 
walther@60328: "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
walther@60328: val xxx = dict_cond_ord var_ord_revPow is_nums;
walther@60328: (*1*)if xxx (eee1, eee1) = EQUAL   then () else error "dict_cond_ord (eee1, eee1) CHANGED";
walther@60328: (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
walther@60328: (*3*)if xxx (eee2, eee1) = LESS    then () else error "dict_cond_ord (eee2, eee1) CHANGED";
walther@60328: (*4*)if xxx (eee2, eee2) = EQUAL   then () else error "dict_cond_ord (eee2, eee2) CHANGED";
walther@60328: 
walther@60328: 
walther@60328: "-------- check make_polynomial with simple terms ----------------------------------------------";
walther@60328: "-------- check make_polynomial with simple terms ----------------------------------------------";
walther@60328: "-------- check make_polynomial with simple terms ----------------------------------------------";
walther@60328: "----- check 1 ---";
walther@60328: val t = TermC.str2term "2*3*a";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
walther@60328: 
walther@60328: "----- check 2 ---";
walther@60328: val t = TermC.str2term "2*a + 3*a";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
walther@60328: 
walther@60328: "----- check 3 ---";
walther@60328: val t = TermC.str2term "2*a + 3*a + 3*a";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
walther@60328: 
walther@60328: "----- check 4 ---";
walther@60328: val t = TermC.str2term "3*a - 2*a";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "a" then () else error "check make_polynomial 4";
walther@60328: 
walther@60328: "----- check 5 ---";
walther@60328: val t = TermC.str2term "4*(3*a - 2*a)";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
walther@60328: 
walther@60328: "----- check 6 ---";
walther@60328: val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
walther@60328: 
walther@60328: "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
walther@60328: val thy = @{theory "Isac_Knowledge"};
walther@60328: "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
walther@60328: val t = TermC.str2term "x \<up> 2 * x";
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
walther@60328: if UnparseC.term t' = "x * x \<up> 2" then ()
walther@60328: else error "poly.sml Poly.is_multUnordered doesn't work";
walther@60328: 
walther@60328: (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
walther@60329: ###  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) +
walther@60328:  (-48 * x \<up> 4 + 8))
walther@60328: ######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
walther@60328: #######  try calc: Poly.is_multUnordered'
walther@60328: =======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
walther@60328: *)
walther@60329: 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))";
walther@60328: 
walther@60328: "----- is_multUnordered ---";
walther@60328: val tsort = sort_variables t;
walther@60329: 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";
walther@60328: is_polyexp t;
walther@60328: tsort = t;
walther@60328: is_polyexp t andalso not (t = sort_variables t);
walther@60328: if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
walther@60328: 
walther@60328: "----- eval_is_multUnordered ---";
walther@60329: 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";
Walther@60509: case eval_is_multUnordered "testid" "" tm @{context} of
walther@60336:     SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
walther@60336:                    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
walther@60336:                           (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
walther@60336:                           Const (\<^const_name>\<open>True\<close>, _))) => ()
walther@60328:   | _ => error "poly.sml diff. eval_is_multUnordered";
walther@60328: 
walther@60328: "----- rewrite_set_ STILL DIDN'T WORK";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt true order_mult_ t;
walther@60328: UnparseC.term t;
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
walther@60328: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
walther@60328: "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
walther@60328: val thy = @{theory "Isac_Knowledge"};
walther@60328: val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
walther@60328: 
walther@60328: (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
walther@60328: (*+*)  andalso not (is_multUnordered arg)
walther@60328: (*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";
walther@60328: 
Walther@60509: case eval_is_multUnordered "xxx " "yyy " t @{context} of
walther@60328:   SOME
walther@60328:     ("xxx 3 * a + - 2 * a_",
walther@60336:       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
walther@60336:         Const (\<^const_name>\<open>False\<close>, _))) => ()
walther@60336: (*      Const (\<^const_name>\<open>True\<close>, _))) => ()   <<<<<--------------------------- this is false*)
walther@60329: | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
walther@60328: 
walther@60328: "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
walther@60328: val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
walther@60328: 
walther@60328: (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
walther@60328: (*+*)  andalso not (is_multUnordered arg)
walther@60328: (*+*)then () else error "sort_variables  - 2 * a   CHANGED";
walther@60328: 
Walther@60509: case eval_is_multUnordered "xxx " "yyy " t @{context} of
walther@60328:   SOME
walther@60328:     ("xxx - 2 * a_",
walther@60336:       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
walther@60336:         Const (\<^const_name>\<open>False\<close>, _))) => ()
walther@60329: | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
walther@60328: 
walther@60328: "----- is_multUnordered --- (a) is_multUnordered = False";
walther@60328: val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
walther@60328: 
walther@60328: (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
walther@60328: (*+*)  andalso not (is_multUnordered arg)
walther@60328: (*+*)then () else error "sort_variables   a   CHANGED";
walther@60328: 
Walther@60509: case eval_is_multUnordered "xxx " "yyy " t @{context} of
walther@60328:   SOME
walther@60328:     ("xxx a_",
walther@60336:       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
walther@60336:         Const (\<^const_name>\<open>False\<close>, _))) => ()
walther@60329: | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
walther@60328: 
walther@60328: "----- is_multUnordered --- (- 2) is_multUnordered = False";
walther@60328: val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
walther@60328: 
walther@60328: (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
walther@60328: (*+*)  andalso not (is_multUnordered arg)
walther@60328: (*+*)then () else error "sort_variables   - 2   CHANGED";
walther@60328: 
Walther@60509: case eval_is_multUnordered "xxx " "yyy " t @{context} of
walther@60328:   SOME
walther@60328:     ("xxx - 2_",
walther@60336:       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
walther@60336:         Const (\<^const_name>\<open>False\<close>, _))) => ()
walther@60329: | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
walther@60328: "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
walther@60328: (*  ca.line 45 of Rewrite.trace_on:
walther@60328: ##  rls: order_mult_rls_ on: 
walther@60328:   x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 
walther@60328: ###  rls: order_mult_ on:
walther@60328:   x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 
walther@60328: ######  rls: Rule_Set.empty-is_multUnordered on: 
walther@60328:   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 
walther@60328: #######  try calc: "Poly.is_multUnordered" 
walther@60328: ########  eval asms: 
walther@60328: 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" 
walther@60328: -------------------------------------------------------------------------------------------------==
walther@60329: 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" 
walther@60328: #######  calc. to: True 
walther@60328: #######  try calc: "Poly.is_multUnordered" 
walther@60328: #######  try calc: "Poly.is_multUnordered" 
walther@60328: ###  rls: order_mult_ on: 
walther@60328: N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2))  +  3 * (a \<up> 2 * (x * (- 1) \<up> 2))  +  a \<up> 3 * (- 1) \<up> 3 
walther@60328: --------+--------------------------+---------------------------------+---------------------------<>
walther@60329: O:x \<up> 3 + - 1  * (3 * (a * x \<up> 2))  +  - 1 \<up> 2 * (3 * (a \<up> 2 * x))     +  - 1 \<up> 3 * a \<up> 3 
walther@60328: -------------------------------------------------------------------------------------------------<>
walther@60328: *)
walther@60328: 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";
walther@60328: (*
walther@60328: "~~~~~ fun is_multUnordered
walther@60328: "~~~~~~~ fun sort_variables
walther@60328: "~~~~~~~~~ val sort_varList
walther@60328: *)
walther@60328: "~~~~~ fun is_multUnordered , args:"; val (t) = (t);
walther@60328:      is_polyexp t = true;
walther@60328: 
walther@60328:   val return =
walther@60328:              sort_variables t;
walther@60328: (*+*)if UnparseC.term return =
walther@60328: (*+*)  "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"
walther@60328: (*+*)then () else error "sort_variables  x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
walther@60328: 
walther@60328: "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
walther@60328:   	val ll = map monom2list (poly2list t);
walther@60328:   	val lls = map sort_varList ll; 
walther@60328: 
walther@60328: (*+*)val ori3 = nth 3 ll;
walther@60328: (*+*)val mon3 = nth 3 lls;
walther@60328: 
walther@60328: (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
walther@60328: (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
walther@60328: (*+*)if UnparseC.terms ori3       = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
walther@60328: (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
walther@60328: 
walther@60328: (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
walther@60328: (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
walther@60328: (*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
walther@60328: (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
walther@60328: 
walther@60328: "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
walther@60328: (* Output below with:
walther@60328: val sort_varList = sort var_ord;
walther@60328: fun var_ord (a,b: term) = 
walther@60328: (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
walther@60328:    sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
walther@60328:   prod_ord string_ord string_ord 
walther@60328:   ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
walther@60328: );
walther@60328: *)
walther@60328: (*+*)val xxx = sort_varList ori3;
walther@60328: (*
walther@60328: {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
walther@60328: {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
walther@60328:       
walther@60328: isa                                            isa2
walther@60328: {a = "var_ord ", a_b = "(3, x)"}               {a = "var_ord ", a_b = "(3, x)"}
walther@60328:   {sort_args = "(|||, ||||||), (x, ---)"}        {sort_args = "(|||, ||||||), (x, ---)"}
walther@60328: {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
walther@60328:   {sort_args = "(x, ---), (|||, ||||||)"}        {sort_args = "(x, ---), (|||, ||||||)"}
walther@60328: {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}   {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
walther@60328:   {sort_args = "(|||, ||||||), (a, 2)"}          {sort_args = "(|||, ||||||), (a, |||)"}
walther@60328:                                   ^^^                                             ^^^
walther@60328: 
walther@60328: {a = "var_ord ", a_b = "(x, a \<up> 2)"}           {a = "var_ord ", a_b = "(x, a \<up> 2)"}
walther@60328:   {sort_args = "(x, ---), (a, 2)"}               {sort_args = "(x, ---), (a, |||)"}
walther@60328:                              ^^^                                             ^^^
walther@60328: {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
walther@60328:   {sort_args = "(x, ---), (|||, ||||||)"}        {sort_args = "(x, ---), (|||, ||||||)"}
walther@60328: {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}       {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
walther@60328:   {sort_args = "(|||, ||||||), (|||, ||||||)"}   {sort_args = "(|||, ||||||), (|||, ||||||)"}
walther@60328: *)
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
walther@60328: "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
walther@60328: "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
walther@60328: val t = TermC.str2term "b * a * a";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if UnparseC.term t = "a \<up> 2 * b" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 21";
walther@60328: 
walther@60328: "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
walther@60328:     ((is_polyexp t) andalso not (t = sort_variables t)) = true;  (*isa == isa2*)
walther@60328: 
walther@60328: (*+*)if    is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
walther@60336: "~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (t);
walther@60328:     (*if*) TermC.is_num num (*else*);
walther@60328: 
walther@60336: "~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (num);
walther@60328:     (*if*) TermC.is_num num (*else*);
walther@60328:       (*if*) TermC.is_variable num (*then*);
walther@60328: 
walther@60328:                            val xxx = sort_variables t;
walther@60328: (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
walther@60328: 
walther@60328: 
walther@60328: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
walther@60328: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
walther@60328: "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
walther@60328: val t = TermC.str2term "2*3*a";
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
walther@60328: (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
walther@60328: (*
walther@60328: ##  try calc: "Groups.times_class.times" 
walther@60328: ##  rls: order_mult_rls_ on: 6 * a 
walther@60328: ###  rls: order_mult_ on: 6 * a 
walther@60328: ######  rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered 
walther@60328: #######  try calc: "Poly.is_multUnordered" 
walther@60328: ########  eval asms: "6 * a is_multUnordered = True"    (*isa*)
walther@60328:                                              = False"   (*isa2*)
walther@60328: #######  calc. to: True  (*isa*)
walther@60328:                    False (*isa2*)
walther@60328: *)
walther@60328: val t = TermC.str2term "(6 * a) is_multUnordered"; 
walther@60328: val SOME
walther@60328:     (_, t') =
Walther@60509:            eval_is_multUnordered "xxx" () t @{context};
walther@60328: (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () 
walther@60328: (*+*)else error "6 * a is_multUnordered = False CHANGED";
walther@60328: 
walther@60328: "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
walther@60336: 		       (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory});
walther@60328:     (*if*) is_multUnordered arg (*else*);
walther@60328: 
walther@60328: "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
walther@60328:   val return =
walther@60328:      ((is_polyexp t) andalso not (t = sort_variables t));
walther@60328: 
walther@60328: (*+*)return = false;                                             (*isa*)
walther@60328: (*+*)  is_polyexp t = true;                                      (*isa*)
walther@60328: (*+*)                        not (t = sort_variables t) = false; (*isa*)
walther@60328: 
walther@60328:                             val xxx = sort_variables t;
walther@60328: (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
walther@60328: 
walther@60328: "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
walther@60328: "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
walther@60328: "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
walther@60328: val thy = @{theory AlgEin};
Walther@60424: val ctxt = Proof_Context.init_global thy;
walther@60328: 
Walther@60500: val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
walther@60328: (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
walther@60328: if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
walther@60328: then ((*norm_Poly NOT COMPLETE -- TODO MG*))
walther@60328: else error "norm_Poly changed behavior";
walther@60328: (* isa:
walther@60328: ##  rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben 
walther@60328: ###  rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben 
walther@60328: ######  rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
walther@60328: oben is_addUnordered 
walther@60328: #######  try calc: "Poly.is_addUnordered" 
walther@60328: ########  eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
walther@60328: oben is_addUnordered = True" 
walther@60328: #######  calc. to: True 
walther@60328: #######  try calc: "Poly.is_addUnordered" 
walther@60328: #######  try calc: "Poly.is_addUnordered" 
walther@60328: ###  rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben 
walther@60328: *)
walther@60328: "~~~~~ fun sort_monoms , args:"; val (t) =
walther@60328:   (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
walther@60328: (*+*)val t' =
walther@60328:            sort_monoms t;
walther@60328: (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
walther@60328: 
walther@60328: 
walther@60328: "-------- complex examples from textbook Schalk I ----------------------------------------------";
walther@60328: "-------- complex examples from textbook Schalk I ----------------------------------------------";
walther@60328: "-------- complex examples from textbook Schalk I ----------------------------------------------";
walther@60329: val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60329: if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 9b";
walther@60328: 
walther@60328: "-----SPB Schalk I p.64 No.296a ---";
walther@60328: val t = TermC.str2term "(x - a) \<up> 3";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60329: if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 10";
walther@60328: 
walther@60328: "-----SPB Schalk I p.64 No.296c ---";
walther@60328: val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60329: if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 11";
walther@60328: 
walther@60328: "-----SPB Schalk I p.62 No.242c ---";
walther@60329: val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if (UnparseC.term t) = "1"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 12";
walther@60328: 
walther@60328: "-----SPB Schalk I p.60 No.209a ---";
walther@60328: val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if UnparseC.term t = "a \<up> 7"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 13";
walther@60328: 
walther@60328: "-----SPB Schalk I p.60 No.209d ---";
walther@60328: val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if UnparseC.term t = "d \<up> 3"
walther@60328: then () else error "poly.sml: diff.behav. in make_polynomial 14";
walther@60328: 
walther@60328: 
walther@60328: "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
walther@60328: "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
walther@60328: "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
walther@60328: "-----SPO ---";
walther@60329: val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if UnparseC.term t = "1" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 15";
walther@60328: 
walther@60328: "-----SPO ---";
walther@60329: val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if UnparseC.term t = "a \<up> 2" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 18";
walther@60328: "-----SPO ---";
walther@60329: val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if (UnparseC.term t) = "1" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 19";
walther@60328: "-----SPO ---";
walther@60328: val t = TermC.str2term "b + a - b";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if (UnparseC.term t) = "a" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 20";
walther@60328: 
walther@60328: "-----SPO ---";
Walther@60424: val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
walther@60328: if (UnparseC.term t) = "a \<up> 4" then ()
walther@60328: else error "poly.sml: diff.behav. in make_polynomial 24";