1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Wed Aug 23 19:19:42 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Thu Aug 24 12:51:16 2006 +0200
1.3 @@ -1,7 +1,6 @@
1.4 (* chapter 'Biegelinie' from the textbook:
1.5 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
1.6 - authors: Walther Neuper
1.7 - 050826,
1.8 + authors: Walther Neuper 2005
1.9 (c) due to copyright terms
1.10
1.11 use"IsacKnowledge/Biegelinie.ML";
2.1 --- a/src/sml/IsacKnowledge/Poly.ML Wed Aug 23 19:19:42 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Poly.ML Thu Aug 24 12:51:16 2006 +0200
2.3 @@ -1,13 +1,51 @@
2.4 -(*
2.5 +(*.eval_funs, rulesets, problems and methods concerning polynamials
2.6 + authors: Matthias Goldgruber 2003
2.7 + (c) due to copyright terms
2.8 +
2.9 use"../IsacKnowledge/Poly.ML";
2.10 use"IsacKnowledge/Poly.ML";
2.11 use"Poly.ML";
2.12
2.13 remove_thy"Poly";
2.14 use_thy"IsacKnowledge/Isac";
2.15 - *)
2.16 -"******* Poly.ML begin *******";
2.17 +****************************************************************.*)
2.18
2.19 +(*.****************************************************************
2.20 + remark on 'polynomials'
2.21 + WN020919
2.22 + there are 5 kinds of expanded normalforms:
2.23 +[1] 'complete polynomial' (Komplettes Polynom), univariate
2.24 + a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
2.25 + not (a_n = 0), some a_i may be zero (DON'T disappear),
2.26 + variables in monomials lexicographically ordered and complete,
2.27 + x written as 1*x^1, ...
2.28 +[2] 'polynomial' (Polynom), univariate and multivariate
2.29 + a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
2.30 + 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
2.31 + not (a_n = 0), some a_i may be zero (ie. monomials disappear),
2.32 + exponents and coefficients equal 1 are not shown,
2.33 + and variables in monomials are lexicographically ordered
2.34 + examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
2.35 + [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
2.36 + [2]: "x + (-50) * x ^^^ 3"
2.37 + [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
2.38 +
2.39 +[3] 'expanded_term' (Ausmultiplizierter Term):
2.40 + pull out unary minus to binary minus,
2.41 + as frequently exercised in schools; other conditions for [2] hold however
2.42 + examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
2.43 + "4 * x ^^^ 2 - 9 * y ^^^ 2"
2.44 +[4] 'polynomial_in' (Polynom in):
2.45 + polynomial in 1 variable with arbitrary coefficients
2.46 + examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
2.47 + "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
2.48 +[5] 'expanded_in' (Ausmultiplizierter Termin in):
2.49 + analoguous to [3] with binary minus like [3]
2.50 + examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
2.51 + "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
2.52 +*****************************************************************.*)
2.53 +
2.54 +"******** Poly.ML begin ******************************************";
2.55 theory' := overwritel (!theory', [("Poly.thy",Poly.thy)]);
2.56
2.57
3.1 --- a/src/sml/IsacKnowledge/Poly.sml Wed Aug 23 19:19:42 2006 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,74 +0,0 @@
3.4 -(* remark on 'polynomials'
3.5 - WN.19.9.02
3.6 - there are 5 kinds of expanded normalforms:
3.7 -[1] 'complete polynomial' (Komplettes Polynom), univariate
3.8 - a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
3.9 - not (a_n = 0), some a_i may be zero (DON'T disappear),
3.10 - variables in monomials lexicographically ordered and complete,
3.11 - x written as 1*x^1, ...
3.12 -[2] 'polynomial' (Polynom), univariate and multivariate
3.13 - a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
3.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
3.15 - not (a_n = 0), some a_i may be zero (ie. monomials disappear),
3.16 - exponents and coefficients equal 1 are not shown,
3.17 - and variables in monomials are lexicographically ordered
3.18 - examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
3.19 - [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
3.20 - [2]: "x + (-50) * x ^^^ 3"
3.21 - [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
3.22 -
3.23 -[3] 'expanded_term' (Ausmultiplizierter Term):
3.24 - pull out unary minus to binary minus,
3.25 - as frequently exercised in schools; other conditions for [2] hold however
3.26 - examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
3.27 - "4 * x ^^^ 2 - 9 * y ^^^ 2"
3.28 -[4] 'polynomial_in' (Polynom in):
3.29 - polynomial in 1 variable with arbitrary coefficients
3.30 - examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
3.31 - "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
3.32 -[5] 'expanded_in' (Ausmultiplizierter Termin in):
3.33 - analoguous to [3] with binary minus like [3]
3.34 - examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
3.35 - "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
3.36 -
3.37 -*)
3.38 -
3.39 -
3.40 -val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
3.41 -atomty t;
3.42 -(*** -------------
3.43 -*** Const ( Trueprop, bool => prop)
3.44 -*** . Const ( op =, [real, real] => bool)
3.45 -*** . . Const ( op -, [real, real] => real)
3.46 -*** . . . Const ( 0, real)
3.47 -*** . . . Var ((x, 0), real)
3.48 -*** . . Const ( uminus, real => real)
3.49 -*** . . . Var ((x, 0), real) *)
3.50 -
3.51 -val t = (term_of o the o (parse thy)) "-1";
3.52 -atomty t;
3.53 -(*** -------------
3.54 -*** Free ( -1, real) *)
3.55 -val t = (term_of o the o (parse thy)) "- 1";
3.56 -atomty t;
3.57 -(*** -------------
3.58 -*** Const ( uminus, real => real)
3.59 -*** . Free ( 1, real) *)
3.60 -
3.61 -val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
3.62 -atomty t;
3.63 -(**** -------------
3.64 -*** Free ( -x, real)*)
3.65 -val t = (term_of o the o (parse thy)) "- x";
3.66 -atomty t;
3.67 -(**** -------------
3.68 -*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
3.69 -val t = (term_of o the o (parse thy)) "-(x)";
3.70 -atomty t;
3.71 -(**** -------------
3.72 -*** Free ( -x, real)*)
3.73 -
3.74 -
3.75 -
3.76 -
3.77 -
4.1 --- a/src/sml/IsacKnowledge/Rational.ML Wed Aug 23 19:19:42 2006 +0200
4.2 +++ b/src/sml/IsacKnowledge/Rational.ML Thu Aug 24 12:51:16 2006 +0200
4.3 @@ -4,66 +4,47 @@
4.4 TU-Graz SS 2002
4.5 Use is subject to license terms.
4.6
4.7 -Remark on notions in the documentation below:
4.8 +use"IsacKnowledge/Rational.ML";
4.9 +use"Rational.ML";
4.10 +
4.11 +remove_thy"Rational";
4.12 +use_thy"IsacKnowledge/Isac";
4.13 +****************************************************************.*)
4.14 +
4.15 +(*.*****************************************************************
4.16 + Remark on notions in the documentation below:
4.17 referring to the remark on 'polynomials' in Poly.sml we use
4.18 - (2) 'polynomial' normalform (Polynom)
4.19 - (3) 'expanded_term' normalform (Ausmultiplizierter Term),
4.20 - where normalform (2) is a special case of (3), i.e. (3) implies (2).
4.21 + [2] 'polynomial' normalform (Polynom)
4.22 + [3] 'expanded_term' normalform (Ausmultiplizierter Term),
4.23 + where normalform [2] is a special case of [3], i.e. [3] implies [2].
4.24 Instead of
4.25 - 'fraction with numerator and nominator both in normalform (2)'
4.26 - 'fraction with numerator and nominator both in normalform (3)'
4.27 + 'fraction with numerator and nominator both in normalform [2]'
4.28 + 'fraction with numerator and nominator both in normalform [3]'
4.29 we say:
4.30 - 'fraction in normalform (2)'
4.31 - 'fraction in normalform (3)'
4.32 + 'fraction in normalform [2]'
4.33 + 'fraction in normalform [3]'
4.34 or
4.35 - 'fraction (2)'
4.36 - 'fraction (3)'.
4.37 + 'fraction [2]'
4.38 + 'fraction [3]'.
4.39 a 'simple fraction' is a term with '/' as outmost operator and
4.40 - numerator and nominator in normalform (2) or (3).
4.41 -.*)
4.42 + numerator and nominator in normalform [2] or [3].
4.43 +****************************************************************.*)
4.44
4.45 signature RATIONALI =
4.46 sig
4.47 - type mv_monom (*.internal representation .*)
4.48 - type mv_poly (*.internal representation .*)
4.49 - val add_fraction_ : (*.add 2 or more fractions .*)
4.50 - theory -> (*.10.02 unused .*)
4.51 - term -> (*.2 or more fractions with normalform (3) .*)
4.52 - (term * (*.one fraction in normalform (3) WN0210??? .*)
4.53 - term list) (*.eventual assumptions in normalform (3) WN0210???.*)
4.54 - option (*.None: the function is not applicable .*)
4.55 - val add_fraction_p_ :(*.add 2 or more fractions .*)
4.56 - theory -> (*.10.02 unused .*)
4.57 - term -> (*.2 or more fractions with normalform (2) .*)
4.58 - (term * (*.one fraction with normalform (2) .*)
4.59 - term list) (*.eventual assumptions in normalform (2) WN0210???.*)
4.60 - option (*.None: the function is not applicable .*)
4.61 - val calculate_Rational :
4.62 - rls (*.simplifies expressions with numerals .*)
4.63 - val calc_rat_erls:rls(*.evaluates conditions in calculate_Rational .*)
4.64 - val cancel : rls (*.cancels a single fraction in normalform (3).
4.65 - resulting in a canceled fraction (3) .*)
4.66 - val cancel_ : (*.cancels a single fraction .*)
4.67 - theory -> (*.10.02 unused .*)
4.68 - term -> (*.fraction in normalform (3) .*)
4.69 - (term * (*.fraction in normalform (3) .*)
4.70 - term list) (*.eventual asumptions in normalform (3) .*)
4.71 - option (*.None: the function is not applicable .*)
4.72 - val cancel_p : rls (*.cancels a single fraction with normalform (2)
4.73 - resulting in a canceled fraction (2) .*)
4.74 - val cancel_p_ :
4.75 - theory ->
4.76 - term ->
4.77 - (term *
4.78 - term list)
4.79 - option
4.80 - val common_nominator :
4.81 - rls (*.transforms sums of at least 2 fractions (3) to
4.82 - sums with the least common multiple as nominator.*)
4.83 + type mv_monom
4.84 + type mv_poly
4.85 + val add_fraction_ : theory -> term -> (term * term list) option
4.86 + val add_fraction_p_ : theory -> term -> (term * term list) option
4.87 + val calculate_Rational : rls
4.88 + val calc_rat_erls:rls
4.89 + val cancel : rls
4.90 + val cancel_ : theory -> term -> (term * term list) option
4.91 + val cancel_p : rls
4.92 + val cancel_p_ : theory -> term -> (term * term list) option
4.93 + val common_nominator : rls
4.94 val common_nominator_ : theory -> term -> (term * term list) option
4.95 - val common_nominator_p :
4.96 - rls (*.transforms sums of at least 2 fractions (2) to
4.97 - sums with the least common multiple as nominator.*)
4.98 + val common_nominator_p : rls
4.99 val common_nominator_p_ : theory -> term -> (term * term list) option
4.100 val eval_is_expanded : string -> 'a -> term -> theory ->
4.101 (string * term) option
4.102 @@ -77,27 +58,28 @@
4.103 val mv_lcm : mv_poly -> mv_poly -> mv_poly
4.104
4.105 val norm_expanded_rat_ : theory -> term -> (term * term list) option
4.106 -(*WN.2.6.pull into struct !!!
4.107 +(*WN0602.2.6.pull into struct !!!
4.108 val norm_Rational : rls(*.normalizes an arbitrary rational term without
4.109 roots into a simple and canceled fraction
4.110 - with normalform (2).*)
4.111 + with normalform [2].*)
4.112 *)
4.113 (*val norm_rational_p : 19.10.02 missing FIXXXXXXXXXXXXME
4.114 - rls (*.normalizes an rational term (2) without
4.115 + rls (*.normalizes an rational term [2] without
4.116 roots into a simple and canceled fraction
4.117 - with normalform (2).*)
4.118 + with normalform [2].*)
4.119 *)
4.120 val norm_rational_ : theory -> term -> (term * term list) option
4.121 val polynomial2expanded : term -> term option
4.122 val rational_erls :
4.123 rls (*.evaluates an arbitrary rational term with numerals.*)
4.124
4.125 -(*???????? WN-->SK fehlen Funktionen, die exportiert werden sollen ? *)
4.126 +(*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)
4.127 end
4.128
4.129 -(*.survey on the functions
4.130 - ~~~~~~~~~~~~~~~~~~~~~~~
4.131 - (2) 'polynomial' :rls | (3)'expanded_term':rls
4.132 +(*.**************************************************************************
4.133 +survey on the functions
4.134 +~~~~~~~~~~~~~~~~~~~~~~~
4.135 + [2] 'polynomial' :rls | [3]'expanded_term':rls
4.136 --------------------:------------------+-------------------:-----------------
4.137 factout_p_ : | factout_ :
4.138 cancel_p_ : | cancel_ :
4.139 @@ -107,7 +89,7 @@
4.140 :common_nominator_p| :common_nominator
4.141 add_fraction_p_ : | add_fraction_ :
4.142 --------------------:------------------+-------------------:-----------------
4.143 -??? :norm_rational_p | :norm_rational
4.144 +???SK :norm_rational_p | :norm_rational
4.145
4.146 This survey shows only the principal functions for reuse, and the identifiers
4.147 of the rls exported. The list below shows some more useful functions.
4.148 @@ -122,7 +104,7 @@
4.149 expanded2polynomial = ...
4.150
4.151 remark: polynomial2expanded o expanded2polynomial = I,
4.152 - where 'o' is function chaining, and 'I' is identity ??????WN?????????
4.153 + where 'o' is function chaining, and 'I' is identity WN0210???SK
4.154
4.155 functions for greatest common divisor and canceling
4.156 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.157 @@ -142,13 +124,13 @@
4.158
4.159 functions for normalform of rationals
4.160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.161 -??? interne Funktionen f"ur norm_rational:
4.162 - schaffen diese SML-Funktionen wirklich ganz allgemeine Terme???
4.163 +WN0210???SK interne Funktionen f"ur norm_rational:
4.164 + schaffen diese SML-Funktionen wirklich ganz allgemeine Terme
4.165
4.166 norm_rational_
4.167 norm_expanded_rat_
4.168
4.169 -.*)
4.170 +**************************************************************************.*)
4.171
4.172
4.173 (*##*)
4.174 @@ -161,13 +143,11 @@
4.175 fun gcd_int a b = if b=0 then a
4.176 else gcd_int b (a mod b);
4.177
4.178 -
4.179 (*. univariate polynomials (uv) .*)
4.180 (*. univariate polynomials are represented as a list of the coefficent in reverse maximum degree order .*)
4.181 (*. 5 * x^5 + 4 * x^3 + 2 * x^2 + x + 19 => [19,1,2,4,0,5] .*)
4.182 type uv_poly = int list;
4.183
4.184 -
4.185 (*. adds two uv polynomials .*)
4.186 fun uv_mod_add_poly ([]:uv_poly,p2:uv_poly) = p2:uv_poly
4.187 | uv_mod_add_poly (p1,[]) = p1
4.188 @@ -196,7 +176,7 @@
4.189 )
4.190 end;
4.191
4.192 -(*. calculates the remainder for each element of a integer list divided by p .*)
4.193 +(*.calculates the remainder for each element of a integer list divided by p.*)
4.194 fun uv_mod_list_modp [] p = []
4.195 | uv_mod_list_modp (x::xs) p = (uv_mod_mod2(x,p))::(uv_mod_list_modp xs p);
4.196
4.197 @@ -615,8 +595,9 @@
4.198 val LEX_=0; (* lexicographical term order *)
4.199 val GGO_=1; (* greatest degree order *)
4.200
4.201 -(*. datatypes .*)
4.202 -type mv_monom = (int * int list); (* (coefficient,list of exponents) *)
4.203 +(*. datatypes for internal representation.*)
4.204 +type mv_monom = (int * (*.coefficient or the monom.*)
4.205 + int list); (*.list of exponents) .*)
4.206 type mv_poly = mv_monom list;
4.207
4.208 (*. help function for monom_greater and geq .*)
4.209 @@ -1347,7 +1328,7 @@
4.210 if count_neg(tl(the(term2coef' t (get_vars(t)))))=0 then true
4.211 else false;
4.212
4.213 -(*. checks for expanded term (3) .*)
4.214 +(*. checks for expanded term [3] .*)
4.215 fun is_expanded t = test_exp t " " andalso check_coeff(t);
4.216
4.217 (*WN.7.3.03 Hilfsfunktion f"ur term2poly'*)
4.218 @@ -1459,7 +1440,7 @@
4.219
4.220 (*. translates an Isabelle term into internal representation.
4.221 term2poly
4.222 - fn : term -> (*normalform (2) *)
4.223 + fn : term -> (*normalform [2] *)
4.224 string list -> (*for ...!!! BITTE DIE ERKLÄRUNG,
4.225 DIE DU MIR LETZTES MAL GEGEBEN HAST*)
4.226 mv_monom list (*internal representation *)
4.227 @@ -2326,7 +2307,7 @@
4.228
4.229 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon
4.230 -------------------------------------------------------------
4.231 -(* FIXME brauch ma des überhaupt??? *)
4.232 +(* WN0210???SK brauch ma des überhaupt *)
4.233 fun com_den2(x::xs,denom,den,var)=
4.234 let
4.235 val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
4.236 @@ -2370,7 +2351,7 @@
4.237 )
4.238 end;
4.239
4.240 -(* FIXME brauch ma des überhaupt??? *)
4.241 +(* WN0210???SK brauch ma des überhaupt *)
4.242 fun com_den_exp2(x::xs,denom,den,var)=
4.243 let
4.244 val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
4.245 @@ -2556,7 +2537,7 @@
4.246
4.247 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon
4.248 -------------------------------------------------------------
4.249 -(* FIXME brauch ma des überhaupt??? *)
4.250 +(* WN0210???SK brauch ma des überhaupt *)
4.251 fun step_add_list_of_fractions2 []=(Free("0",HOLogic.realT),[]:term list)
4.252 | step_add_list_of_fractions2 [x]=(x,[])
4.253 | step_add_list_of_fractions2 (xs) =
4.254 @@ -2574,7 +2555,7 @@
4.255 )
4.256 end;
4.257
4.258 -(* FIXME brauch ma des überhaupt??? *)
4.259 +(* WN0210???SK brauch ma des überhaupt *)
4.260 fun step_add_list_of_fractions2_exp []=(Free("0",HOLogic.realT),[]:term list)
4.261 | step_add_list_of_fractions2_exp [x]=(x,[])
4.262 | step_add_list_of_fractions2_exp (xs) =
4.263 @@ -2613,23 +2594,42 @@
4.264 raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
4.265 | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
4.266
4.267 -(*. cancels a single fraction .*)
4.268 +(*.factors out the gcd of nominator and denominator:
4.269 + a/b = (a' * gcd)/(b' * gcd), a,b,gcd are poly[2].*)
4.270 fun factout_p_ (thy:theory) t = Some (step_cancel t,[]:term list);
4.271 fun factout_ (thy:theory) t = Some (step_cancel_expanded t,[]:term list);
4.272 +
4.273 +(*.cancels a single fraction with normalform [2]
4.274 + resulting in a canceled fraction [2], see factout_ .*)
4.275 fun cancel_p_ (thy:theory) t = (*WN.2.6.03 no rewrite -> None !*)
4.276 (let val (t',asm) = direct_cancel(*_expanded ... corrected MG.21.8.03*) t
4.277 in if t = t' then None else Some (t',asm)
4.278 end) handle _ => None;
4.279 +(*.the same as above with normalform [3]
4.280 + val cancel_ :
4.281 + theory -> (*10.02 unused *)
4.282 + term -> (*fraction in normalform [3] *)
4.283 + (term * (*fraction in normalform [3] *)
4.284 + term list) (*casual asumptions in normalform [3] *)
4.285 + option (*None: the function is not applicable *).*)
4.286 fun cancel_ (thy:theory) t = Some (direct_cancel_expanded t) handle _ => None;
4.287
4.288 -(*. calculates the common nominator.*)
4.289 +(*.transforms sums of at least 2 fractions [3] to
4.290 + sums with the least common multiple as nominator.*)
4.291 fun common_nominator_p_ (thy:theory) t =
4.292 ((*writeln("### common_nominator_p_ called");*)
4.293 Some (step_add_list_of_fractions(term2list(t))) handle _ => None
4.294 );
4.295 -
4.296 fun common_nominator_ (thy:theory) t =
4.297 Some (step_add_list_of_fractions_exp(term2list(t))) handle _ => None;
4.298 +
4.299 +(*.add 2 or more fractions
4.300 +val add_fraction_p_ :
4.301 + theory -> (*10.02 unused *)
4.302 + term -> (*2 or more fractions with normalform [2] *)
4.303 + (term * (*one fraction with normalform [2] *)
4.304 + term list) (*casual assumptions in normalform [2] WN0210???SK *)
4.305 + option (*None: the function is not applicable *).*)
4.306 fun add_fraction_p_ (thy:theory) t =
4.307 (writeln("### add_fraction_p_ called");
4.308 (let val ts = term2list t
4.309 @@ -2638,7 +2638,7 @@
4.310 else None (*raise error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
4.311 end) handle _ => None
4.312 );
4.313 -
4.314 +(*.same as add_fraction_p_ but with normalform [3].*)
4.315 (*Some (step_add_list_of_fractions2(term2list(t))); *)
4.316 fun add_fraction_ (thy:theory) t =
4.317 if length(term2list(t))>1
4.318 @@ -2660,7 +2660,8 @@
4.319 Some (add_list_of_fractions_exp(term2list(t))) handle _ => None;
4.320
4.321
4.322 -(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
4.323 +(*.evaluates conditions in calculate_Rational.*)
4.324 +(*make local with FIXX@ME result:term *term list*)
4.325 val calc_rat_erls = prep_rls(
4.326 Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
4.327 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *)
4.328 @@ -2673,7 +2674,8 @@
4.329 scr = EmptyScr});
4.330
4.331
4.332 -(*.does NOT rearrange the term by AC-rewriting; thus terms with variables
4.333 +(*.simplifies expressions with numerals;
4.334 + does NOT rearrange the term by AC-rewriting; thus terms with variables
4.335 need to have constants to be commuted together respectively.*)
4.336 val calculate_Rational = prep_rls(
4.337 merge_rls "calculate_Rational"
4.338 @@ -2748,11 +2750,11 @@
4.339
4.340 (*.3 'reverse-rewrite-sets' for symbolic computation on rationals:
4.341 =================================================================
4.342 - (A2) 'cancel_p': .
4.343 - (A3) 'cancel': .
4.344 - (B2) 'common_nominator_p': transforms summands in a term (2)
4.345 + A[2] 'cancel_p': .
4.346 + A[3] 'cancel': .
4.347 + B[2] 'common_nominator_p': transforms summands in a term [2]
4.348 to fractions with the (least) common multiple as nominator.
4.349 - (3) 'norm_rational': normalizes arbitrary algebraic terms (without
4.350 + B[3] 'norm_rational': normalizes arbitrary algebraic terms (without
4.351 radicals and transzendental functions) to one canceled fraction,
4.352 nominator and denominator in polynomial form.
4.353
4.354 @@ -2766,9 +2768,9 @@
4.355
4.356
4.357 local(*. cancel_p
4.358 -------------------------.
4.359 -cancel transforms a fraction consisting of two (uni- or multivariate)
4.360 -polynomials into another such fraction; examples:
4.361 +------------------------
4.362 +cancels a single fraction consisting of two (uni- or multivariate)
4.363 +polynomials WN0609???SK[2] into another such a fraction; examples:
4.364
4.365 a^2 + (-1)*b^2 a + b
4.366 -------------------- = ---------
4.367 @@ -2779,21 +2781,12 @@
4.368 a 1
4.369
4.370 Remark: the reverse ruleset does _NOT_ work properly with other input !.*)
4.371 -(*WN 24.8.02: wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)
4.372 -
4.373 -
4.374 -(*
4.375 -val {rules=rules,rew_ord=(_,ro),...} =
4.376 - rep_rls (the (assoc'(!ruleset',"make_polynomial")));
4.377 -*)
4.378 +(*WN020824 wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)
4.379 +
4.380 val {rules=rules,rew_ord=(_,ro),...} =
4.381 rep_rls (assoc_rls "make_polynomial");
4.382 val thy = Rational.thy;
4.383
4.384 -
4.385 -(*.cancel_p_ = fn : theory -> term -> (term * term list) option
4.386 - as defined above*)
4.387 -
4.388 (*.init_state = fn : term -> istate
4.389 initialzies the state of the script interpreter. The state is:
4.390
4.391 @@ -2920,8 +2913,8 @@
4.392
4.393 local(*.ad (1) 'cancel'
4.394 ------------------------------
4.395 -cancel transforms a fraction consisting of two binoms (binary - !)
4.396 -into another such fraction; examples:
4.397 +cancels a single fraction consisting of two (uni- or multivariate)
4.398 +polynomials WN0609???SK[3] into another such a fraction; examples:
4.399
4.400 a^2 - b^2 a + b
4.401 -------------------- = ---------
4.402 @@ -3001,7 +2994,7 @@
4.403
4.404
4.405
4.406 -local(*.ad (2) 'common_nominator_p'
4.407 +local(*.ad [2] 'common_nominator_p'
4.408 ---------------------------------
4.409 FIXME Beschreibung .*)
4.410
4.411 @@ -3150,7 +3143,7 @@
4.412 end;(*local*)
4.413
4.414
4.415 -local(*.ad (2) 'common_nominator'
4.416 +local(*.ad [2] 'common_nominator'
4.417 ---------------------------------
4.418 FIXME Beschreibung .*)
4.419
4.420 @@ -3311,7 +3304,6 @@
4.421 open RationalI;
4.422 (*##*)
4.423
4.424 -
4.425 (*.the expression contains + - * ^ / only ?.*)
4.426 fun is_ratpolyexp (Free _) = true
4.427 | is_ratpolyexp (Const ("op +",_) $ Free _ $ Free _) = true
4.428 @@ -3418,7 +3410,7 @@
4.429 rules = [Thm ("rat_mult",num_str rat_mult),
4.430 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
4.431 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
4.432 - (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be (2),
4.433 + (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
4.434 otherwise inv.to a / b / c = ...*)
4.435 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
4.436 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
4.437 @@ -3461,7 +3453,8 @@
4.438 (*"0 / ?x = 0"*)
4.439 ], scr = EmptyScr}:rls);
4.440
4.441 -(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
4.442 +(*erls for calculate_Rational;
4.443 + make local with FIXX@ME result:term *term list WN0609???SKMG*)
4.444 val norm_rat_erls = prep_rls(
4.445 Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
4.446 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
4.447 @@ -3509,7 +3502,7 @@
4.448 theory' := overwritel (!theory', [("Rational.thy",Rational.thy)]);
4.449
4.450
4.451 -(*WN.18.3.03 ???: simplifies all but cancel and common_nominator*)
4.452 +(*WN030318???SK: simplifies all but cancel and common_nominator*)
4.453 val simplify_rational =
4.454 merge_rls "simplify_rational" expand_binoms
4.455 (append_rls "divide" calculate_Rational
4.456 @@ -3518,7 +3511,7 @@
4.457 Thm ("rat_mult",num_str rat_mult),
4.458 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
4.459 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
4.460 - (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be (2),
4.461 + (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
4.462 otherwise inv.to a / b / c = ...*)
4.463 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
4.464 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
4.465 @@ -3564,7 +3557,7 @@
4.466 scr = EmptyScr});
4.467 (* -------------------------------------------------------------------- *)
4.468 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
4.469 - used in initial part norm_Rational_mg, see example MG-DiplArb.p.60 .*)
4.470 + used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
4.471 val rat_mult_poly = prep_rls(
4.472 Rls {id = "rat_mult_poly", preconds = [],
4.473 rew_ord = ("dummy_ord",dummy_ord),
4.474 @@ -3580,9 +3573,10 @@
4.475 scr = EmptyScr});
4.476 (* ------------------------------------------------------------------ *)
4.477 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
4.478 - used in looping part norm_Rational_rls, see example MG-DA.p.60
4.479 + used in looping part norm_Rational_rls, see example DA-M02-main.p.60
4.480 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = e_rls,
4.481 - I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Thm APPLIED; WN051028.*)
4.482 + I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Thm APPLIED; WN051028
4.483 + ... WN0609???MG.*)
4.484 val rat_mult_div_pow = prep_rls(
4.485 Rls {id = "rat_mult_div_pow", preconds = [],
4.486 rew_ord = ("dummy_ord",dummy_ord),
4.487 @@ -3681,7 +3675,6 @@
4.488 ("cancel_p_rls", cancel_p_rls)
4.489 ]);
4.490
4.491 -
4.492 calclist':= overwritel (!calclist',
4.493 [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))
4.494 ]);
5.1 --- a/src/sml/RCODE-root.sml Wed Aug 23 19:19:42 2006 +0200
5.2 +++ b/src/sml/RCODE-root.sml Thu Aug 24 12:51:16 2006 +0200
5.3 @@ -76,3 +76,4 @@
5.4 "**** build isac kernel complete *************************";
5.5
5.6 states:=[];
5.7 +print_depth 3;
6.1 --- a/src/sml/ROOT.ML Wed Aug 23 19:19:42 2006 +0200
6.2 +++ b/src/sml/ROOT.ML Thu Aug 24 12:51:16 2006 +0200
6.3 @@ -166,6 +166,7 @@
6.4 "**** run tests on IsacKnowledge complete ****************";
6.5 cd"sml";
6.6 states:=[];
6.7 +print_depth 3;
6.8 "=========================================================";
6.9
6.10 "**** build math-engine complete *************************";
7.1 --- a/src/smltest/IsacKnowledge/poly.sml Wed Aug 23 19:19:42 2006 +0200
7.2 +++ b/src/smltest/IsacKnowledge/poly.sml Thu Aug 24 12:51:16 2006 +0200
7.3 @@ -1,18 +1,19 @@
7.4 (* testexamples for Poly, polynomials
7.5 - author: Matthias Goldgruber
7.6 + author: Matthias Goldgruber 2003
7.7 (c) due to copyright terms
7.8
7.9 use"../smltest/IsacKnowledge/poly.sml";
7.10 use"poly.sml";
7.11 -*)
7.12 +****************************************************************.*)
7.13
7.14 (******************************************************************
7.15 - WN060104 'SPB' come into 'exp_IsacCore_Simp_Poly_Book.xml'
7.16 - 'SPO' come into 'exp_IsacCore_Simp_Poly_Other.xml'
7.17 + WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
7.18 + 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
7.19 *******************************************************************)
7.20 "-----------------------------------------------------------------";
7.21 "table of contents -----------------------------------------------";
7.22 "-----------------------------------------------------------------";
7.23 +"-------- investigate new uniary minus ---------------------------";
7.24 "-------- Bsple aus Schalk I -------------------------------------";
7.25 "-------- Script 'simplification for_polynomials' ----------------";
7.26 "-------- check pbl 'polynomial simplification' -----------------";
7.27 @@ -21,6 +22,48 @@
7.28 "-----------------------------------------------------------------";
7.29 "-----------------------------------------------------------------";
7.30
7.31 +
7.32 +"-------- investigate new uniary minus ---------------------------";
7.33 +"-------- investigate new uniary minus ---------------------------";
7.34 +"-------- investigate new uniary minus ---------------------------";
7.35 +val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
7.36 +atomty t;
7.37 +(*** -------------
7.38 +*** Const ( Trueprop, bool => prop)
7.39 +*** . Const ( op =, [real, real] => bool)
7.40 +*** . . Const ( op -, [real, real] => real)
7.41 +*** . . . Const ( 0, real)
7.42 +*** . . . Var ((x, 0), real)
7.43 +*** . . Const ( uminus, real => real)
7.44 +*** . . . Var ((x, 0), real) *)
7.45 +
7.46 +val t = (term_of o the o (parse thy)) "-1";
7.47 +atomty t;
7.48 +(*** -------------
7.49 +*** Free ( -1, real) *)
7.50 +val t = (term_of o the o (parse thy)) "- 1";
7.51 +atomty t;
7.52 +(*** -------------
7.53 +*** Const ( uminus, real => real)
7.54 +*** . Free ( 1, real) *)
7.55 +
7.56 +val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
7.57 +atomty t;
7.58 +(**** -------------
7.59 +*** Free ( -x, real)*)
7.60 +val t = (term_of o the o (parse thy)) "- x";
7.61 +atomty t;
7.62 +(**** -------------
7.63 +*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
7.64 +val t = (term_of o the o (parse thy)) "-(x)";
7.65 +atomty t;
7.66 +(**** -------------
7.67 +*** Free ( -x, real)*)
7.68 +
7.69 +
7.70 +"-------- Bsple aus Schalk I -------------------------------------";
7.71 +"-------- Bsple aus Schalk I -------------------------------------";
7.72 +"-------- Bsple aus Schalk I -------------------------------------";
7.73 (*SPB Schalk I p.63 No.267b*)
7.74 val t = str2term
7.75 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
8.1 --- a/src/smltest/IsacKnowledge/rational.sml Wed Aug 23 19:19:42 2006 +0200
8.2 +++ b/src/smltest/IsacKnowledge/rational.sml Thu Aug 24 12:51:16 2006 +0200
8.3 @@ -5,7 +5,7 @@
8.4
8.5 use"../smltest/IsacKnowledge/rational.sml";
8.6 use"rational.sml";
8.7 -.*)
8.8 +****************************************************************.*)
8.9
8.10 (******************************************************************
8.11 WN060104 transfer marked (*SR..*)examples to the exp-collection