1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Poly.sml	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,74 @@
     1.4 +(* remark on 'polynomials'
     1.5 +   WN.19.9.02
     1.6 +   there are 5 kinds of expanded normalforms:
     1.7 +[1] 'complete polynomial' (Komplettes Polynom), univariate
     1.8 +   a_0 + a_1.x^1 +...+ a_n.x^n   not (a_n = 0)
     1.9 +	        not (a_n = 0), some a_i may be zero (DON'T disappear),
    1.10 +                variables in monomials lexicographically ordered and complete,
    1.11 +                x written as 1*x^1, ...
    1.12 +[2] 'polynomial' (Polynom), univariate and multivariate
    1.13 +   a_0 + a_1.x +...+ a_n.x^n   not (a_n = 0)
    1.14 +   a_0 + a_1.x_1.x_2^n_12...x_m^n_1m +...+  a_n.x_1^n.x_2^n_n2...x_m^n_nm
    1.15 +	        not (a_n = 0), some a_i may be zero (ie. monomials disappear),
    1.16 +                exponents and coefficients equal 1 are not shown,
    1.17 +                and variables in monomials are lexicographically ordered  
    1.18 +   examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
    1.19 +	     [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
    1.20 +	     [2]: "x + (-50) * x ^^^ 3"
    1.21 +	     [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
    1.22 +
    1.23 +[3] 'expanded_term' (Ausmultiplizierter Term):
    1.24 +   pull out unary minus to binary minus, 
    1.25 +   as frequently exercised in schools; other conditions for [2] hold however
    1.26 +   examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
    1.27 +	     "4 * x ^^^ 2 - 9 * y ^^^ 2"
    1.28 +[4] 'polynomial_in' (Polynom in): 
    1.29 +   polynomial in 1 variable with arbitrary coefficients
    1.30 +   examples: "2 * x + (-50) * x ^^^ 3"                     (poly in x)
    1.31 +	     "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
    1.32 +[5] 'expanded_in' (Ausmultiplizierter Termin in): 
    1.33 +   analoguous to [3] with binary minus like [3]
    1.34 +   examples: "2 * x - 50 * x ^^^ 3"                     (expanded in x)
    1.35 +	     "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
    1.36 +
    1.37 +*)
    1.38 +
    1.39 +
    1.40 +val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
    1.41 +atomty thy t;
    1.42 +(*** -------------
    1.43 +*** Const ( Trueprop, bool => prop)
    1.44 +*** . Const ( op =, [real, real] => bool)
    1.45 +*** . . Const ( op -, [real, real] => real)
    1.46 +*** . . . Const ( 0, real)
    1.47 +*** . . . Var ((x, 0), real)
    1.48 +*** . . Const ( uminus, real => real)
    1.49 +*** . . . Var ((x, 0), real)              *)
    1.50 +
    1.51 +val t = (term_of o the o (parse thy)) "-1";
    1.52 +atomty thy t;
    1.53 +(*** -------------
    1.54 +*** Free ( -1, real)                      *)
    1.55 +val t = (term_of o the o (parse thy)) "- 1";
    1.56 +atomty thy t;
    1.57 +(*** -------------
    1.58 +*** Const ( uminus, real => real)
    1.59 +*** . Free ( 1, real)                     *)
    1.60 +
    1.61 +val t = (term_of o the o (parse thy)) "-x"; (*1-x  syntyx error !!!*)
    1.62 +atomty thy t;
    1.63 +(**** -------------
    1.64 +*** Free ( -x, real)*)
    1.65 +val t = (term_of o the o (parse thy)) "- x";
    1.66 +atomty thy t;
    1.67 +(**** -------------
    1.68 +*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
    1.69 +val t = (term_of o the o (parse thy)) "-(x)";
    1.70 +atomty thy t;
    1.71 +(**** -------------
    1.72 +*** Free ( -x, real)*)
    1.73 +
    1.74 +
    1.75 +
    1.76 +
    1.77 +