1.1 --- a/src/sml/IsacKnowledge/Rational.ML Fri Jul 28 18:54:58 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Rational.ML Wed Aug 23 09:15:43 2006 +0200
1.3 @@ -1,13 +1,8 @@
1.4 -
1.5 -(* use"../IsacKnowledge/Rational.ML";
1.6 - use"IsacKnowledge/Rational.ML";
1.7 - use"Rational.ML";
1.8 - *)
1.9 -
1.10 -(*. calculate in rationals: gcd, lcm, etc.
1.11 - (c) Stefan Karnel
1.12 - Institute for Mathematics D and Institute for Software Technology,
1.13 - TU-Graz SS 2002
1.14 +(*.calculate in rationals: gcd, lcm, etc.
1.15 + (c) Stefan Karnel 2002
1.16 + Institute for Mathematics D and Institute for Software Technology,
1.17 + TU-Graz SS 2002
1.18 + Use is subject to license terms.
1.19
1.20 Remark on notions in the documentation below:
1.21 referring to the remark on 'polynomials' in Poly.sml we use
1.22 @@ -29,34 +24,33 @@
1.23
1.24 signature RATIONALI =
1.25 sig
1.26 - type mv_monom (*.internal representation.*)
1.27 - type mv_poly (*.internal reprecsentation.*)
1.28 - val add_fraction_ : (*.add 2 or more fractions.*)
1.29 - theory -> (*.10.02 unused.*)
1.30 - term -> (*.2 or more fractions with normalform (3).*)
1.31 - (term * (*.one fraction in normalform (3) ?????????WN???*)
1.32 - term list) (*.eventual asumptions in normalform (3) ??????WN???.*)
1.33 - option (*.None: the function is not applicable.*)
1.34 - val add_fraction_p_ :(*.add 2 or more fractions.*)
1.35 - theory -> (*.10.02 unused.*)
1.36 - term -> (*.2 or more fractions with normalform (2).*)
1.37 - (term * (*.one fraction with normalform (2).*)
1.38 - term list) (*.eventual asumptions in normalform (2) ??????WN???.*)
1.39 - option (*.None: the function is not applicable.*)
1.40 + type mv_monom (*.internal representation .*)
1.41 + type mv_poly (*.internal representation .*)
1.42 + val add_fraction_ : (*.add 2 or more fractions .*)
1.43 + theory -> (*.10.02 unused .*)
1.44 + term -> (*.2 or more fractions with normalform (3) .*)
1.45 + (term * (*.one fraction in normalform (3) WN0210??? .*)
1.46 + term list) (*.eventual assumptions in normalform (3) WN0210???.*)
1.47 + option (*.None: the function is not applicable .*)
1.48 + val add_fraction_p_ :(*.add 2 or more fractions .*)
1.49 + theory -> (*.10.02 unused .*)
1.50 + term -> (*.2 or more fractions with normalform (2) .*)
1.51 + (term * (*.one fraction with normalform (2) .*)
1.52 + term list) (*.eventual assumptions in normalform (2) WN0210???.*)
1.53 + option (*.None: the function is not applicable .*)
1.54 val calculate_Rational :
1.55 - rls (*.simplifies expressions with numerals.*)
1.56 - val calc_rat_erls:rls(*for calculate_Rational:make local with
1.57 - FIXXXME result:term * term list*)
1.58 + rls (*.simplifies expressions with numerals .*)
1.59 + val calc_rat_erls:rls(*.evaluates conditions in calculate_Rational .*)
1.60 val cancel : rls (*.cancels a single fraction in normalform (3).
1.61 - resulting in a canceled fraction (3).*)
1.62 - val cancel_ : (*.cancels a single fraction.*)
1.63 - theory -> (*.10.02 unused.*)
1.64 - term -> (*.fraction in normalform (3).*)
1.65 - (term * (*.fraction in normalform (3).*)
1.66 - term list) (*.eventual asumptions in normalform (3).*)
1.67 - option (*.None: the function is not applicable.*)
1.68 + resulting in a canceled fraction (3) .*)
1.69 + val cancel_ : (*.cancels a single fraction .*)
1.70 + theory -> (*.10.02 unused .*)
1.71 + term -> (*.fraction in normalform (3) .*)
1.72 + (term * (*.fraction in normalform (3) .*)
1.73 + term list) (*.eventual asumptions in normalform (3) .*)
1.74 + option (*.None: the function is not applicable .*)
1.75 val cancel_p : rls (*.cancels a single fraction with normalform (2)
1.76 - resulting in a canceled fraction (2).*)
1.77 + resulting in a canceled fraction (2) .*)
1.78 val cancel_p_ :
1.79 theory ->
1.80 term ->
1.81 @@ -3725,3 +3719,9 @@
1.82 "Script SimplifyScript (t_::real) = \
1.83 \ ((Rewrite_Set norm_Rational False) t_)"
1.84 ));
1.85 +
1.86 +(* use"../IsacKnowledge/Rational.ML";
1.87 + use"IsacKnowledge/Rational.ML";
1.88 + use"Rational.ML";
1.89 + *)
1.90 +
2.1 --- a/src/sml/IsacKnowledge/Rational.thy Fri Jul 28 18:54:58 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.thy Wed Aug 23 09:15:43 2006 +0200
2.3 @@ -1,4 +1,7 @@
2.4 -(* rationals, i.e. frcations of multivariate polynomials over the real field
2.5 +(* rationals, i.e. fractions of multivariate polynomials over the real field
2.6 + author: isac team
2.7 + Copyright (c) isac team 2002
2.8 + Use is subject to license terms.
2.9
2.10 depends on Poly (and not on Atools), because
2.11 fractions with _normalized_ polynomials are canceled, added, etc.
2.12 @@ -17,7 +20,7 @@
2.13
2.14 consts
2.15
2.16 - is'_expanded :: "real => bool" ("_ is'_expanded")(*RL->Poly.thy*)
2.17 + is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
2.18 is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
2.19
2.20 rules (*.not contained in Isabelle2002,
3.1 --- a/src/smltest/IsacKnowledge/poly.sml Fri Jul 28 18:54:58 2006 +0200
3.2 +++ b/src/smltest/IsacKnowledge/poly.sml Wed Aug 23 09:15:43 2006 +0200
3.3 @@ -384,8 +384,7 @@
3.4 "-------- interSteps for Schalk 299a -----------------------------";
3.5 states:=[];
3.6 CalcTree
3.7 -[(["term ((x - y)*(x + y))",
3.8 - "normalform N"],
3.9 +[(["term ((x - y)*(x + y))", "normalform N"],
3.10 ("Poly.thy",["polynomial","simplification"],
3.11 ["simplification","for_polynomials"]))];
3.12 Iterator 1;
4.1 --- a/src/smltest/IsacKnowledge/rational.sml Fri Jul 28 18:54:58 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/rational.sml Wed Aug 23 09:15:43 2006 +0200
4.3 @@ -1,6 +1,7 @@
4.4 (*.tests for rationals
4.5 - author: Stefan Karnel 2002
4.6 - (c) isac-team
4.7 + author: Stefan Karnel
4.8 + Copyright (c) Stefan Karnel 2002
4.9 + Use is subject to license terms.
4.10
4.11 use"../smltest/IsacKnowledge/rational.sml";
4.12 use"rational.sml";