wneuper/isa: test/Tools/isac/Knowledge/poly-1.sml@2e0b7ca391dc

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

     2    Author: Walther Neuper

     3    Use is subject to license terms.

     5 Test of basic functions and application to complex examples.

     6 *)

     8 "-----------------------------------------------------------------------------------------------";

     9 "-----------------------------------------------------------------------------------------------";

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

    11 "-----------------------------------------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    26 "-----------------------------------------------------------------------------------------------";

    27 "-----------------------------------------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    48 val thy = @{theory}

    49 val ctxt = Proof_Context.init_global thy

    50 val v = TermC.parseNEW' ctxt "x";

    51 val t = TermC.parseNEW' ctxt "1";

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

    54 val v = TermC.parseNEW' ctxt "AA";

    55 val t = TermC.parseNEW' ctxt "1";

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

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

    59 val v = TermC.parseNEW' ctxt "x";

    60 val t = TermC.parseNEW' ctxt "a*b+c";

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

    63 val v = TermC.parseNEW' ctxt "AA";

    64 val t = TermC.parseNEW' ctxt "a*b+c";

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

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

    68 val v = TermC.parseNEW' ctxt "x";

    69 val t = TermC.parseNEW' ctxt "a*x+c";

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

    72 val v = TermC.parseNEW' ctxt "AA";

    73 val t = TermC.parseNEW' ctxt "a*AA+c";

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

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

    77 val v = TermC.parseNEW' ctxt "x::real";

    78 val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";

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

    81 val v = TermC.parseNEW' ctxt "AA";

    82 val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";

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

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

    86 val v = TermC.parseNEW' ctxt "x::real";

    87 val t = TermC.parseNEW' ctxt "x \<up> 7";

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

    90 val v = TermC.parseNEW' ctxt "AA";

    91 val t = TermC.parseNEW' ctxt "AA \<up> 7";

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

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

    95 val v = TermC.parseNEW' ctxt "x::real";

    96 val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";

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

    99 val v = TermC.parseNEW' ctxt "AA";

   100 val t = TermC.parseNEW' ctxt "(a*b+c)*AA";

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

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

   104 val v = TermC.parseNEW' ctxt "x::real";

   105 val t = TermC.parseNEW' ctxt "(a*b+x)*x";

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

   108 val v = TermC.parseNEW' ctxt "AA";

   109 val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";

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

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

   113 val v = TermC.parseNEW' ctxt "x";

   114 val t = TermC.parseNEW' ctxt "x";

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

   117 val v = TermC.parseNEW' ctxt "AA";

   118 val t = TermC.parseNEW' ctxt "AA";

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

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

   122 val v = TermC.parseNEW' ctxt "x::real";

   123 val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";

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

   126 val v = TermC.parseNEW' ctxt "AA";

   127 val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";

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

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

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

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

   133 val v = TermC.parseNEW' ctxt "x::real";

   135 val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";

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

   138 val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";

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

   141 val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";

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

   144 val t = TermC.parseNEW' ctxt "(a*b+x)*x";

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

   147 val t = TermC.parseNEW' ctxt "x::real";

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

   150 val t = TermC.parseNEW' ctxt "(a*b+c)";

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

   153 val t = TermC.parseNEW' ctxt "ab - (a*b)*x";

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

   156 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)

   157 val thy = @{theory Partial_Fractions}

   158 val ctxt = Proof_Context.init_global thy

   159 val v = TermC.parseNEW' ctxt "AA";

   161 val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";

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

   164 val t = TermC.parseNEW' ctxt "AA \<up> 7";

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

   167 val t = TermC.parseNEW' ctxt "(a*b+c)*AA";

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

   170 val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";

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

   173 val t = TermC.parseNEW' ctxt "AA";

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

   176 val t = TermC.parseNEW' ctxt "(a*b+c)";

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

   179 val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";

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

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

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

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

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

   187 else error "lexicographic order CHANGED";

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

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

   191 val t' =  sort_variables t;

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

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

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

   196   	val ll =  map monom2list (poly2list t);

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

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

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

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

   203   	val lls = map sort_varList ll;

   205 (*+*)case map sort_varList ll of

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

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

   208 (*+*)  ] => ()

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

   211   	val T = type_of t;

   212   	val ls = map (create_monom T) lls;

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

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

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

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

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

   220 (*+*)  ] => ()

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

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

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

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

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

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

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

   231 val t' =     sort_variables t;

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

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

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

   236   	val ll =  map monom2list (poly2list t);

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

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

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

   242   	val lls = map

   243            sort_varList ll;

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

   246 (*+*)      [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*ERROR: NO swap here*)

   247 (*+*)    ] = map sort_varList ll;

   249        map sort_varList ll;

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

   251 val sorted = sort var_ord ts;

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

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

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

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

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

   260 (*+*)then () else error "get_basStr  a  CHANGED";

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

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

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

   266 val ctxt = Proof_Context.init_global @{theory}

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

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

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

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

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

   273 (** )

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

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

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

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

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

   279                                                                               True"   (*isa2*)

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

   281                    True   (*isa2*)

   282 ( **)

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

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

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

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

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

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

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

   292   	val ll =  map monom2list (poly2list t);

   293   	val lls = sort_monList ll;

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

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

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

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

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

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

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

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

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

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

   307 (* isa -- isa2:

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

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

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

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

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

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

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

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

   319 val it = true: bool

   320 val it = true: bool

   321 val it = true: bool

   322 val it = true: bool*)

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

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

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

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

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

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

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

   331 (* isa -- isa2:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   358 val it = true: bool

   359 val it = false: bool

   360 val it = false: bool

   361 val it = true: bool

   362 *)

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

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

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

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

   368   val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =

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

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

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

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

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

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

   376   val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =

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

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

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

   381   val return =

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

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

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

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

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

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

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

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

   391 val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =

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

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

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

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

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

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

   399 val _ = (*the default case*)

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

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

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

   404 val xxx = dict_cond_ord var_ord_revPow is_nums;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   447 val thy = @{theory "Isac_Knowledge"};

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

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

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

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

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

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

   455 ###  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) +

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

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

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

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

   460 *)

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

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

   464 val tsort = sort_variables t;

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

   466 is_polyexp t;

   467 tsort = t;

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

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

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

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

   473 case eval_is_multUnordered "testid" "" tm @{context} of

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

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

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

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

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

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

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

   482 UnparseC.term t;

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

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

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

   488 val thy = @{theory "Isac_Knowledge"};

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

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

   492 (*+*)  andalso not (is_multUnordered arg)

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

   495 case eval_is_multUnordered "xxx " "yyy " t @{context} of

   496   SOME

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

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

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

   500 (*      Const (\<^const_name>\<open>True\<close>, _))) => ()   <<<<<--------------------------- this is false*)

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

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

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

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

   507 (*+*)  andalso not (is_multUnordered arg)

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

   510 case eval_is_multUnordered "xxx " "yyy " t @{context} of

   511   SOME

   512     ("xxx - 2 * a_",

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

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

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

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

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

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

   521 (*+*)  andalso not (is_multUnordered arg)

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

   524 case eval_is_multUnordered "xxx " "yyy " t @{context} of

   525   SOME

   526     ("xxx a_",

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

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

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

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

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

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

   535 (*+*)  andalso not (is_multUnordered arg)

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

   538 case eval_is_multUnordered "xxx " "yyy " t @{context} of

   539   SOME

   540     ("xxx - 2_",

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

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

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

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

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

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

   549 (*  ca.line 45 of Rewrite.trace_on:

   550 ##  rls: order_mult_rls_ on:

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

   552 ###  rls: order_mult_ on:

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

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

   555   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

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

   557 ########  eval asms:

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

   559 -------------------------------------------------------------------------------------------------==

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

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

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

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

   564 ###  rls: order_mult_ on:

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

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

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

   568 -------------------------------------------------------------------------------------------------<>

   569 *)

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

   571 (*

   572 "~~~~~ fun is_multUnordered

   573 "~~~~~~~ fun sort_variables

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

   575 *)

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

   577      is_polyexp t = true;

   579   val return =

   580              sort_variables t;

   581 (*+*)if UnparseC.term return =

   582 (*+*)  "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"

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

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

   586   	val ll = map monom2list (poly2list t);

   587   	val lls = map sort_varList ll;

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

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

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

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

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

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

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

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

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

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

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

   603 (* Output below with:

   604 val sort_varList = sort var_ord;

   605 fun var_ord (a,b: term) =

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

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

   608   prod_ord string_ord string_ord

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

   610 );

   611 *)

   612 (*+*)val xxx = sort_varList ori3;

   613 (*

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

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

   617 isa                                            isa2

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

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

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

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

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

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

   624                                   ^^^                                             ^^^

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

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

   628                              ^^^                                             ^^^

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

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

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

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

   633 *)

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

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

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

   639 val t = TermC.str2term "b * a * a";

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

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

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

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

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

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

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

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

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

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

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

   655                            val xxx = sort_variables t;

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

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

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

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

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

   663 val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;

   664 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";

   665 (*

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

   667 ##  rls: order_mult_rls_ on: 6 * a

   668 ###  rls: order_mult_ on: 6 * a

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

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

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

   672                                              = False"   (*isa2*)

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

   674                    False (*isa2*)

   675 *)

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

   677 val SOME

   678     (_, t') =

   679            eval_is_multUnordered "xxx" () t @{context};

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

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

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

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

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

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

   688   val return =

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

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

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

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

   695                             val xxx = sort_variables t;

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

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

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

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

   701 val thy = @{theory AlgEin};

   702 val ctxt = Proof_Context.init_global thy;

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

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

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

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

   708 else error "norm_Poly changed behavior";

   709 (* isa:

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

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

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

   713 oben is_addUnordered

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

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

   716 oben is_addUnordered = True"

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

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

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

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

   721 *)

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

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

   724 (*+*)val t' =

   725            sort_monoms t;

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

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

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

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

   732 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";

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

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

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

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

   738 val t = TermC.str2term "(x - a) \<up> 3";

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

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

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

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

   744 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";

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

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

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

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

   750 val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";

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

   752 if (UnparseC.term t) = "1"

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

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

   756 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   774 if UnparseC.term t = "1" then ()

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

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

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

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

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

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

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

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

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

   785 if (UnparseC.term t) = "1" then ()

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

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

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

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

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

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

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

   794 val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";

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

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

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

author	wneuper <Walther.Neuper@jku.at>
	Thu, 04 Aug 2022 12:48:37 +0200
changeset 60509	2e0b7ca391dc
parent 60500	59a3af532717
child 60565	f92963a33fe3
permissions	-rw-r--r--