wneuper/isa: test/Tools/isac/Knowledge/poly-1.sml@8fa678b678e8

     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 = ParseC.parse_test @{context} "x / x";

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

    36 val t = ParseC.parse_test @{context} "- 1 * A * 3";

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

    39 val t = ParseC.parse_test @{context} "- 1 * AA * 3";

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

    42 val t = ParseC.parse_test @{context} "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 = ParseC.parse_test ctxt "x";

    51 val t = ParseC.parse_test ctxt "1";

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

    54 val v = ParseC.parse_test ctxt "AA";

    55 val t = ParseC.parse_test ctxt "1";

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

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

    59 val v = ParseC.parse_test ctxt "x";

    60 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

    64 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x";

    69 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

    73 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

    78 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

    82 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

    87 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

    91 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

    96 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

   100 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

   105 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

   109 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x";

   114 val t = ParseC.parse_test ctxt "x";

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

   117 val v = ParseC.parse_test ctxt "AA";

   118 val t = ParseC.parse_test ctxt "AA";

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

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

   122 val v = ParseC.parse_test ctxt "x::real";

   123 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

   127 val t = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

   135 val t = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test ctxt "x::real";

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

   150 val t = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

   161 val t = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test ctxt "AA";

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

   176 val t = ParseC.parse_test 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 = ParseC.parse_test 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 @{context} 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 @{context} (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 @{context} 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 @{context} 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 @{context} ts = "[- 2, a]" andalso UnparseC.terms @{context} sorted = "[- 2, a]"

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

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

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

   259 (*+*)if UnparseC.term @{context} (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 = ParseC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";

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

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

   270 if UnparseC.term @{context} 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 (ParseC.parse_test @{context} "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) = (ParseC.parse_test @{context} "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 @{context}) lls = ["[x \<up> 3, y]", "[x \<up> 2, y \<up> 2]"];

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

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

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

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

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

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

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

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

   306 (* isa -- isa2:

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

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

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

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

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

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

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

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

   318 val it = true: bool

   319 val it = true: bool

   320 val it = true: bool

   321 val it = true: bool*)

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

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

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

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

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

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

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

   330 (* isa -- isa2:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   357 val it = true: bool

   358 val it = false: bool

   359 val it = false: bool

   360 val it = true: bool

   361 *)

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

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

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

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

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

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

   369 (*+*)UnparseC.term @{context} x = "x \<up> 2";

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

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

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

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

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

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

   377 (*+*)UnparseC.term @{context} x = "y \<up> 2";

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

   380   val return =

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

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

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

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

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

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

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

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

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

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

   392 (*+*)UnparseC.term @{context} x = "x \<up> 3";

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

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

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

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

   398 val _ = (*the default case*)

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

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

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

   403 val xxx = dict_cond_ord var_ord_revPow is_nums;

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

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

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

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

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

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

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

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

   414 val t = ParseC.parse_test @{context} "2*3*a";

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

   416 if UnparseC.term @{context} t = "6 * a" then () else error "check make_polynomial 1";

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

   419 val t = ParseC.parse_test @{context} "2*a + 3*a";

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

   421 if UnparseC.term @{context} t = "5 * a" then () else error "check make_polynomial 2";

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

   424 val t = ParseC.parse_test @{context} "2*a + 3*a + 3*a";

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

   426 if UnparseC.term @{context} t = "8 * a" then () else error "check make_polynomial 3";

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

   429 val t = ParseC.parse_test @{context} "3*a - 2*a";

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

   431 if UnparseC.term @{context} t = "a" then () else error "check make_polynomial 4";

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

   434 val t = ParseC.parse_test @{context} "4*(3*a - 2*a)";

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

   436 if UnparseC.term @{context} t = "4 * a" then () else error "check make_polynomial 5";

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

   439 val t = ParseC.parse_test @{context} "4*(3*a \<up> 2 - 2*a \<up> 2)";

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

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

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

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

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

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

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

   448 val t = ParseC.parse_test @{context} "x \<up> 2 * x";

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

   450 if UnparseC.term @{context} t' = "x * x \<up> 2" then ()

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

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

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

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

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

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

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

   459 *)

   460 val t = ParseC.parse_test @{context} "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))";

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

   463 val tsort = sort_variables t;

   464 UnparseC.term @{context} 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";

   465 is_polyexp t;

   466 tsort = t;

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

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

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

   471 val tm = ParseC.parse_test @{context} "(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";

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

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

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

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

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

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

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

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

   481 UnparseC.term @{context} t;

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

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

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

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

   488 val t as (_ $ arg) = ParseC.parse_test @{context} "(3 * a + - 2 * a) is_multUnordered";

   490 (*+*)if UnparseC.term @{context} (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true

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

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

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

   495   SOME

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

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

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

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

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

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

   503 val t as (_ $ arg) = ParseC.parse_test @{context} "(- 2 * a) is_multUnordered";

   505 (*+*)if UnparseC.term @{context} (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true

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

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

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

   510   SOME

   511     ("xxx - 2 * a_",

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

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

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

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

   517 val t as (_ $ arg) = ParseC.parse_test @{context} "(a) is_multUnordered";

   519 (*+*)if UnparseC.term @{context} (sort_variables arg) = "a" andalso is_polyexp arg = true

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

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

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

   524   SOME

   525     ("xxx a_",

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

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

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

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

   531 val t as (_ $ arg) = ParseC.parse_test @{context} "(- 2) is_multUnordered";

   533 (*+*)if UnparseC.term @{context} (sort_variables arg) = "- 2" andalso is_polyexp arg = true

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

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

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

   538   SOME

   539     ("xxx - 2_",

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

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

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

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

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

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

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

   549 ##  rls: order_mult_rls_ on:

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

   551 ###  rls: order_mult_ on:

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

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

   554   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

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

   556 ########  eval asms:

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

   558 -------------------------------------------------------------------------------------------------==

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

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

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

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

   563 ###  rls: order_mult_ on:

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

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

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

   567 -------------------------------------------------------------------------------------------------<>

   568 *)

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

   570 (*

   571 "~~~~~ fun is_multUnordered

   572 "~~~~~~~ fun sort_variables

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

   574 *)

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

   576      is_polyexp t = true;

   578   val return =

   579              sort_variables t;

   580 (*+*)if UnparseC.term @{context} return =

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

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

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

   585   	val ll = map monom2list (poly2list t);

   586   	val lls = map sort_varList ll;

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

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

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

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

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

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

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

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

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

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

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

   602 (* Output below with:

   603 val sort_varList = sort var_ord;

   604 fun var_ord (a,b: term) =

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

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

   607   prod_ord string_ord string_ord

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

   609 );

   610 *)

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

   612 (*

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

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

   616 isa                                            isa2

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

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

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

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

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

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

   623                                   ^^^                                             ^^^

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

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

   627                              ^^^                                             ^^^

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

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

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

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

   632 *)

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

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

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

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

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

   640 if UnparseC.term @{context} t = "a \<up> 2 * b" then ()

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

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

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

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

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

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

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

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

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

   654                            val xxx = sort_variables t;

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

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

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

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

   661 val t = ParseC.parse_test @{context} "2*3*a";

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

   663 (*+*)if UnparseC.term @{context} t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";

   664 (*

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

   666 ##  rls: order_mult_rls_ on: 6 * a

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

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

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

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

   671                                              = False"   (*isa2*)

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

   673                    False (*isa2*)

   674 *)

   675 val t = ParseC.parse_test @{context} "(6 * a) is_multUnordered";

   676 val SOME

   677     (_, t') =

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

   679 (*+*)if UnparseC.term @{context} t' = "6 * a is_multUnordered = False" then ()

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

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

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

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

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

   687   val return =

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

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

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

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

   694                             val xxx = sort_variables t;

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

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

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

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

   700 val thy = @{theory AlgEin};

   701 val ctxt = Proof_Context.init_global thy;

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

   704 (ParseC.parse_test @{context} "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");

   705 if UnparseC.term @{context} f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"

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

   707 else error "norm_Poly changed behavior";

   708 (* isa:

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

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

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

   712 oben is_addUnordered

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

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

   715 oben is_addUnordered = True"

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

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

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

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

   720 *)

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

   722   (ParseC.parse_test @{context} "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");

   723 (*+*)val t' =

   724            sort_monoms t;

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

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

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

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

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

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

   733 if (UnparseC.term @{context} t) = "1 + - 2 * x \<up> 4 + x \<up> 8"

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

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

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

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

   739 if (UnparseC.term @{context} t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"

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

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

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

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

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

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

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

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

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

   751 if (UnparseC.term @{context} t) = "1"

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

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

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

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

   757 if UnparseC.term @{context} t = "a \<up> 7"

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

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

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

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

   763 if UnparseC.term @{context} t = "d \<up> 3"

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

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

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

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

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

   771 val t = ParseC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";

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

   773 if UnparseC.term @{context} t = "1" then ()

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

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

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

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

   779 if UnparseC.term @{context} t = "a \<up> 2" then ()

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

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

   782 val t = ParseC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";

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

   784 if (UnparseC.term @{context} t) = "1" then ()

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

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

   787 val t = ParseC.parse_test @{context} "b + a - b";

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

   789 if (UnparseC.term @{context} t) = "a" then ()

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

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

   793 val t = ParseC.parse_test ctxt "a \<up> 2 * (-a) \<up> 2";

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

   795 if (UnparseC.term @{context} t) = "a \<up> 4" then ()

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

author	wneuper <Walther.Neuper@jku.at>
	Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789	8fa678b678e8
parent 60675	d841c720d288
permissions	-rw-r--r--