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