1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Sat Aug 24 11:23:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Sat Aug 24 11:54:39 2013 +0200
     1.3 @@ -22,6 +22,9 @@
     1.4  "-------- ... missing WN060103 --------------------------";
     1.5  "-------- fun monom2term,  fun poly2term' ---------------";
     1.6  "~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
     1.7 +"-------- fun poly_of_term ---------------------------------------------------";
     1.8 +"-------- fun is_poly --------------------------------------------------------";
     1.9 +"-------- fun term_of_poly ---------------------------------------------------";
    1.10  "-------- and app_rev --------------------------------------------------------";
    1.11  "-------- external calculating functions test -----------";
    1.12  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
    1.13 @@ -306,6 +309,65 @@
    1.14   val SOME t' = polynomial2expanded t; term2str t';
    1.15  "1 - x ^^^ 2 - 5 * x ^^^ 5";
    1.16  
    1.17 +"-------- fun poly_of_term ---------------------------------------------------";
    1.18 +"-------- fun poly_of_term ---------------------------------------------------";
    1.19 +(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
    1.20 +"-------- fun poly_of_term ---------------------------------------------------";
    1.21 +val vs = "12 * x^^^3 * y^^^4 * z^^^6" |> str2term |> vars |> map free2str |> sort string_ord;
    1.22 +
    1.23 +if poly_of_term vs (str2term "12::real") = SOME [(12, [0, 0, 0])]
    1.24 +then () else error "poly_of_term 1 changed";
    1.25 +if poly_of_term vs (str2term "x::real") = SOME [(1, [1, 0, 0])]
    1.26 +then () else error "poly_of_term 2 changed";
    1.27 +if poly_of_term vs (str2term "12 * x^^^3") = SOME [(12, [3, 0, 0])]
    1.28 +then () else error "poly_of_term 3 changed";
    1.29 +if poly_of_term vs (str2term "12 * x^^^3 * y^^^4 * z^^^6") = SOME [(12, [3, 4, 6])]
    1.30 +then () else error "poly_of_term 4 changed";
    1.31 +if poly_of_term vs (str2term "1 + 2 * x^^^3 * y^^^4 * z^^^6 + y") =
    1.32 +  SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
    1.33 +then () else error "poly_of_term 5 changed";
    1.34 +
    1.35 +(*poly_of_term is quite liberal:*)
    1.36 +(*the coefficient may be somewhere, the order of variables and the parentheses 
    1.37 +  within a monomial are arbitrary*)
    1.38 +if poly_of_term vs (str2term "y^^^4 * (x^^^3 * 12 * z^^^6)") = SOME [(12, [3, 4, 6])]
    1.39 +then () else error "poly_of_term 6 changed";
    1.40 +
    1.41 +(*there may even be more than 1 coefficient:*)
    1.42 +if poly_of_term vs (str2term "2 * y^^^4 * (x^^^3 * 6 * z^^^6)") = SOME [(12, [3, 4, 6])]
    1.43 +then () else error "poly_of_term 7 changed";
    1.44 +
    1.45 +(*the order and the parentheses within monomials are arbitrary:*)
    1.46 +if poly_of_term vs (str2term "2 * x^^^3 * y^^^4 * z^^^6 + (7 * y^^^8 + 1)")
    1.47 +  = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
    1.48 +then () else error "poly_of_term 8 changed";
    1.49 +============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
    1.50 +
    1.51 +"-------- fun is_poly --------------------------------------------------------";
    1.52 +"-------- fun is_poly --------------------------------------------------------";
    1.53 +(*========== inhibit exn WN130822 TODO =========================================================
    1.54 +"-------- fun is_poly --------------------------------------------------------";
    1.55 +if is_poly (str2term "2 * x^^^3 * y^^^4 * z^^^6 + 7 * y^^^8 + 1")
    1.56 +then () else error "is_poly 1 changed";
    1.57 +if not (is_poly (str2term "2 * (x^^^3 * y^^^4 * z^^^6 + 7) * y^^^8 + 1"))
    1.58 +then () else error "is_poly 2 changed";
    1.59 +============ inhibit exn WN130822 TODO ========================================================*)
    1.60 +
    1.61 +"-------- fun term_of_poly ---------------------------------------------------";
    1.62 +"-------- fun term_of_poly ---------------------------------------------------";
    1.63 +(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
    1.64 +"-------- fun term_of_poly ---------------------------------------------------";
    1.65 +val expT = HOLogic.realT
    1.66 +val Free (_, baseT) = (hd o vars o str2term) "12 * x^^^3 * y^^^4 * z^^^6";
    1.67 +val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
    1.68 +val vs = ["x","y","z"]
    1.69 +(*precondition for [(c, es),...]: legth es = length vs*)
    1.70 +;
    1.71 +if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
    1.72 +then () else error "term_of_poly 1 changed";
    1.73 +============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
    1.74 +
    1.75 +
    1.76  "-------- and app_rev --------------------------------------------------------";
    1.77  "-------- and app_rev --------------------------------------------------------";
    1.78  "-------- and app_rev --------------------------------------------------------";