wneuper/isa: test/Tools/isac/Knowledge/poly-1.sml@0c10aeff57d7

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   155 val thy = @{theory Partial_Fractions}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   184 else error "lexicographic order CHANGED";

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

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

   188 val t' =  sort_variables t;

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

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

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

   193   	val ll =  map monom2list (poly2list t);

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

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

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

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

   200   	val lls = map sort_varList ll;

   202 (*+*)case map sort_varList ll of

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

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

   205 (*+*)  ] => ()

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

   208   	val T = type_of t;

   209   	val ls = map (create_monom T) lls;

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

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

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

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

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

   217 (*+*)  ] => ()

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

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

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

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

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

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

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

   228 val t' =     sort_variables t;

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

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

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

   233   	val ll =  map monom2list (poly2list t);

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

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

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

   239   	val lls = map

   240            sort_varList ll;

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

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

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

   246        map sort_varList ll;

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

   248 val sorted = sort var_ord ts;

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

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

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

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

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

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

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

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

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

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

   264 Rewrite.trace_on := false;

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

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

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

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

   270 (** )

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

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

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

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

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

   276                                                                               True"   (*isa2*)

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

   278                    True   (*isa2*)

   279 ( **)

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

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

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

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

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

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

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

   289   	val ll =  map monom2list (poly2list t);

   290   	val lls = sort_monList ll;

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

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

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

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

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

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

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

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

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

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

   304 (* isa -- isa2:

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

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

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

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

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

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

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

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

   316 val it = true: bool

   317 val it = true: bool

   318 val it = true: bool

   319 val it = true: bool*)

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

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

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

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

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

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

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

   328 (* isa -- isa2:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   355 val it = true: bool

   356 val it = false: bool

   357 val it = false: bool

   358 val it = true: bool

   359 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   378   val return =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   396 val _ = (*the default case*)

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

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

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

   401 val xxx = dict_cond_ord var_ord_revPow is_nums;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   457 *)

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

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

   461 val tsort = sort_variables t;

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

   463 is_polyexp t;

   464 tsort = t;

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

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

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

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

   470 case eval_is_multUnordered "testid" "" tm thy of

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

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

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

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

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

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

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

   479 UnparseC.term t;

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

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

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

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

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

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

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

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

   492 case eval_is_multUnordered "xxx " "yyy " t thy of

   493   SOME

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

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

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

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

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

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

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

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

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

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

   507 case eval_is_multUnordered "xxx " "yyy " t thy of

   508   SOME

   509     ("xxx - 2 * a_",

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

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

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

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

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

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

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

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

   521 case eval_is_multUnordered "xxx " "yyy " t thy of

   522   SOME

   523     ("xxx a_",

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

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

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

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

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

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

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

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

   535 case eval_is_multUnordered "xxx " "yyy " t thy of

   536   SOME

   537     ("xxx - 2_",

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

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

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

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

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

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

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

   547 ##  rls: order_mult_rls_ on:

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

   549 ###  rls: order_mult_ 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: Rule_Set.empty-is_multUnordered 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 is_multUnordered

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

   554 ########  eval asms:

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

   556 -------------------------------------------------------------------------------------------------==

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

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

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

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

   561 ###  rls: order_mult_ on:

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

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

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

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

   566 *)

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

   568 (*

   569 "~~~~~ fun is_multUnordered

   570 "~~~~~~~ fun sort_variables

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

   572 *)

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

   574      is_polyexp t = true;

   576   val return =

   577              sort_variables t;

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

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

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

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

   583   	val ll = map monom2list (poly2list t);

   584   	val lls = map sort_varList ll;

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

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

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

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

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

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

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

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

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

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

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

   600 (* Output below with:

   601 val sort_varList = sort var_ord;

   602 fun var_ord (a,b: term) =

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

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

   605   prod_ord string_ord string_ord

   606   ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

   607 );

   608 *)

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

   610 (*

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

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

   614 isa                                            isa2

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

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

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

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

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

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

   621                                   ^^^                                             ^^^

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

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

   625                              ^^^                                             ^^^

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

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

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

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

   630 *)

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

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

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

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

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

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

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

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

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

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

   645 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);

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

   648 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);

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

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

   652                            val xxx = sort_variables t;

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

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

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

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

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

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

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

   662 (*

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

   664 ##  rls: order_mult_rls_ on: 6 * a

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

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

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

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

   669                                              = False"   (*isa2*)

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

   671                    False (*isa2*)

   672 *)

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

   674 val SOME

   675     (_, t') =

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

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

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

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

   681 		       (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});

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

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

   685   val return =

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

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

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

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

   692                             val xxx = sort_variables t;

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

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

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

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

   698 val thy = @{theory AlgEin};

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

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

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

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

   704 else error "norm_Poly changed behavior";

   705 (* isa:

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

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

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

   709 oben is_addUnordered

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

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

   712 oben is_addUnordered = True"

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

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

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

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

   717 *)

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

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

   720 (*+*)val t' =

   721            sort_monoms t;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

author	wneuper <walther.neuper@jku.at>
	Sat, 17 Jul 2021 14:05:28 +0200
changeset 60329	0c10aeff57d7
parent 60328	cc02d2cc2e24
child 60330	e5e9a6c45597
permissions	-rw-r--r--