1.1 --- a/src/sml/IsacKnowledge/Rational.ML Tue Sep 05 15:06:55 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Rational.ML Tue Sep 05 16:06:48 2006 +0200
1.3 @@ -1006,6 +1006,7 @@
1.4 (*. step-depth is 1 and if the result is not an integerpolynomial .*)
1.5 (*. this function returns [] .*)
1.6 fun mv_newton ([]:(mv_poly) list) = []:mv_poly
1.7 + | mv_newton ([mp]:(mv_poly) list) = mp:mv_poly
1.8 | mv_newton pl =
1.9 let
1.10 val c=ref pl;
1.11 @@ -1029,7 +1030,6 @@
1.12 while hd(!c1)=[] do c1:=tl(!c1);
1.13 c1:=rev(!c1);
1.14 ppl:= !c1;
1.15 -
1.16 mv_newton_add (!c1) 1
1.17 end;
1.18
1.19 @@ -1055,6 +1055,13 @@
1.20 )
1.21 end;
1.22
1.23 +(*. checks if all elements of the list have value zero .*)
1.24 +fun list_is_null [] = true
1.25 + | list_is_null (x::xs) = (x=0 andalso list_is_null(xs));
1.26 +
1.27 +(* check if main variable is zero*)
1.28 +fun main_zero (ms : mv_poly) = (list_is_null o (map (hd o #2))) ms;
1.29 +
1.30 (*. calculates the content of an polynomial .*)
1.31 fun mv_content([]:mv_poly) = []:mv_poly
1.32 | mv_content(p1) =
1.33 @@ -1107,23 +1114,45 @@
1.34 and mv_gcd ([]:mv_poly) ([]:mv_poly) :mv_poly= []:mv_poly
1.35 | mv_gcd ([]:mv_poly) (p2) :mv_poly= p2:mv_poly
1.36 | mv_gcd (p1:mv_poly) ([]) :mv_poly= p1:mv_poly
1.37 - | mv_gcd ([(x,xs)]:mv_poly) ([(y,ys)]):mv_poly = if xs=ys then [((gcd_int x y),xs)]
1.38 - else
1.39 - (
1.40 - [((gcd_int x y),(map uv_mod_min)(xs~~ys))]:mv_poly
1.41 - )
1.42 - | mv_gcd (p1:mv_poly) ([(y,ys)]) :mv_poly= [(gcd_int (uv_content2(p1)) (y),(map uv_mod_min)(mv_min_pp(p1)~~ys))]:mv_poly
1.43 - | mv_gcd ([(y,ys)]:mv_poly) (p2):mv_poly = [(gcd_int (uv_content2(p2)) (y),(map uv_mod_min)(mv_min_pp(p2)~~ys))]:mv_poly
1.44 + | mv_gcd ([(x,xs)]:mv_poly) ([(y,ys)]):mv_poly =
1.45 + let
1.46 + val xpoly:mv_poly = [(x,xs)];
1.47 + val ypoly:mv_poly = [(y,ys)];
1.48 + in
1.49 + (
1.50 + if xs=ys then [((gcd_int x y),xs)]
1.51 + else [((gcd_int x y),(map uv_mod_min)(xs~~ys))]:mv_poly
1.52 + )
1.53 + end
1.54 + | mv_gcd (p1:mv_poly) ([(y,ys)]) :mv_poly=
1.55 + (
1.56 + [(gcd_int (uv_content2(p1)) (y),(map uv_mod_min)(mv_min_pp(p1)~~ys))]:mv_poly
1.57 + )
1.58 + | mv_gcd ([(y,ys)]:mv_poly) (p2):mv_poly =
1.59 + (
1.60 + [(gcd_int (uv_content2(p2)) (y),(map uv_mod_min)(mv_min_pp(p2)~~ys))]:mv_poly
1.61 + )
1.62 | mv_gcd (p1':mv_poly) (p2':mv_poly):mv_poly=
1.63 let
1.64 val vc=length(#2(hd(p1')));
1.65 - val cont=mv_gcd (mv_content(p1')) (mv_content(p2'));
1.66 + val cont =
1.67 + (
1.68 + if main_zero(mv_content(p1')) andalso
1.69 + (main_zero(mv_content(p2'))) then
1.70 + mv_correct((mv_gcd (mv_cut(mv_content(p1'))) (mv_cut(mv_content(p2')))),0)
1.71 + else
1.72 + mv_gcd (mv_content(p1')) (mv_content(p2'))
1.73 + );
1.74 val p1= #1(mv_division(p1',cont,LEX_));
1.75 val p2= #1(mv_division(p2',cont,LEX_));
1.76 val gcd=ref [];
1.77 val candidate=ref [];
1.78 val interpolation_list=ref [];
1.79 val delta=ref [];
1.80 + val p1r = ref [];
1.81 + val p2r = ref [];
1.82 + val p1r' = ref [];
1.83 + val p2r' = ref [];
1.84 val factor=ref [];
1.85 val r=ref 0;
1.86 val gcd_r=ref [];
1.87 @@ -1141,10 +1170,23 @@
1.88 while !exit=0 do
1.89 (
1.90 r:=(!r)+1;
1.91 - delta:=mv_gcd (mv_lc(p1,LEX_)) (mv_lc(p2,LEX_));
1.92 - if mv_shorten(mv_subs(mv_lc(p1,LEX_),!r),LEX_)=[] andalso
1.93 - mv_shorten(mv_subs(mv_lc(p2,LEX_),!r),LEX_)=[]
1.94 - then ()
1.95 + p1r := mv_lc(p1,LEX_);
1.96 + p2r := mv_lc(p2,LEX_);
1.97 + if main_zero(!p1r) andalso
1.98 + main_zero(!p2r)
1.99 + then
1.100 + (
1.101 + delta := mv_correct((mv_gcd (mv_cut (!p1r)) (mv_cut (!p2r))),0)
1.102 + )
1.103 + else
1.104 + (
1.105 + delta := mv_gcd (!p1r) (!p2r)
1.106 + );
1.107 + if mv_shorten(mv_subs(!p1r,!r),LEX_)=[] andalso
1.108 + mv_shorten(mv_subs(!p2r,!r),LEX_)=[]
1.109 + then
1.110 + (
1.111 + )
1.112 else
1.113 (
1.114 gcd_r:=mv_shorten(mv_gcd (mv_shorten(mv_subs(p1,!r),LEX_))
1.115 @@ -1166,10 +1208,9 @@
1.116 else ()
1.117 )
1.118 );
1.119 -
1.120 if length(!interpolation_list)> uv_mod_min(mv_deg(p1),mv_deg(p2)) then
1.121 (
1.122 - candidate:=mv_newton(rev(!interpolation_list));
1.123 + candidate := mv_newton(rev(!interpolation_list));
1.124 if !candidate=[] then ()
1.125 else
1.126 (
1.127 @@ -1464,10 +1505,6 @@
1.128 (*. same as expanded2poly with automatic detection of the variables .*)
1.129 fun expanded2polyx t = expanded2poly t (((map free2str) o vars) t);
1.130
1.131 -(*. checks if all elements of the list have value zero .*)
1.132 -fun list_is_null [] = true
1.133 - | list_is_null (x::xs) = (x=0 andalso list_is_null(xs));
1.134 -
1.135 (*. converts a powerproduct into term representation .*)
1.136 fun powerproduct2term(xs,v) =
1.137 let
1.138 @@ -1534,17 +1571,10 @@
1.139 )
1.140 )
1.141 );*)
1.142 -(*WN.10.3.03*)
1.143 -fun allzeros [] = true
1.144 - | allzeros (i::is) = if i = 0 then allzeros is else false;
1.145 -(*allzeros [0,0,0,0];
1.146 -val it = true
1.147 - allzeros [0,0,1,0];
1.148 -val it = false
1.149 - allzeros [];
1.150 -val it = true*)
1.151 +
1.152 +
1.153 (*fun monom2term ((i, is):mv_monom, v) =
1.154 - if allzeros is
1.155 + if list_is_null is
1.156 then
1.157 if i >= 0
1.158 then Free (str_of_int i, HOLogic.realT)
1.159 @@ -1560,7 +1590,7 @@
1.160 Free ((str_of_int o abs) i, HOLogic.realT)) $
1.161 powerproduct2term(is, vs);---------------------------*)
1.162 fun monom2term ((i, is) : mv_monom, vs) =
1.163 - if allzeros is
1.164 + if list_is_null is
1.165 then Free (str_of_int i, HOLogic.realT)
1.166 else if i = 1
1.167 then powerproduct2term (is, vs)
2.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 15:06:55 2006 +0200
2.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:06:48 2006 +0200
2.3 @@ -1042,7 +1042,7 @@
2.4 (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*)
2.5 (*... takes uncredible much time:*)
2.6 (*
2.7 -WN060831???SK6
2.8 +WN060831????SK6
2.9 "----- SK060904-2a non-termination of add_fraction_p_";
2.10 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
2.11 val None = rewrite_set_ thy false common_nominator_p t;
2.12 @@ -1052,7 +1052,7 @@
2.13 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
2.14 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
2.15 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n";
2.16 -WN060831???SK7
2.17 +WN060831????SK7
2.18 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
2.19 val None = add_fraction_p_ thy t;
2.20 *)
2.21 @@ -1152,7 +1152,7 @@
2.22
2.23 (*Schalk I, p.60 Nr. 215c *)
2.24 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter kürzen!!!*)
2.25 -(* WN060831???MG1
2.26 +(* WN060831????MG1
2.27 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
2.28 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.29 term2str t;
2.30 @@ -1341,13 +1341,13 @@
2.31 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
2.32
2.33 (*Schalk I, p.68 Nr. 437a *)
2.34 -(* SK loops: rechnet ewig; cancel_p hängt sich auf... WN060420???MG4
2.35 +(* SK loops: rechnet ewig; cancel_p hängt sich auf... WN060420????MG4
2.36 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
2.37 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.38 term2str t;
2.39 *)
2.40
2.41 -(*SK loops .. WN060420???MG5 not canceled to "1 / (4*c + 3*e)"*)
2.42 +(*SK loops .. WN060420????MG5 not canceled to "1 / (4*c + 3*e)"*)
2.43 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
2.44 val Some (t',_) = rewrite_set_ thy false make_polynomial t;
2.45 term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)";
2.46 @@ -1355,7 +1355,7 @@
2.47 "----- SK060904-1b non-termination of cancel_p_";
2.48 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
2.49 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
2.50 -(* WN060831???SK8
2.51 +(* WN060831????SK8
2.52 val Some (t',_) = rewrite_set_ thy false cancel_p t'';
2.53 term2str t';
2.54 *)
2.55 @@ -1364,14 +1364,14 @@
2.56 (* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter kürzen!!!
2.57 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
2.58 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.59 -term2str t; WN060831???SK9
2.60 +term2str t; WN060831????SK9
2.61 "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
2.62
2.63 *)
2.64
2.65 (*
2.66 val t = str2term
2.67 -"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)"; WN060831???SK10
2.68 +"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)"; WN060831????SK10
2.69 val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.70 term2str t;
2.71 uncaught exception nonexhaustive binding failure
2.72 @@ -1409,7 +1409,7 @@
2.73 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
2.74
2.75 (*Schalk I, p.68 Nr. 440b *)
2.76 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831???SK11
2.77 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831????SK11
2.78 val t = str2term
2.79 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
2.80 trace_rewrite := true;
2.81 @@ -1430,7 +1430,7 @@
2.82 (3 * a ^^^ 3 * b + -3 * a * b ^^^ 3 + a ^^^ 4 * b + -1 * a ^^^ 2 * b ^^^ 3)";
2.83 val Some (t',_) = rewrite_set_ thy false cancel_p t;
2.84 term2str t';
2.85 -WN060831???SK12*)
2.86 +WN060831????SK12*)
2.87
2.88 "-------- common denominator and multiplication ------------------";
2.89 "-------- common denominator and multiplication ------------------";
2.90 @@ -1549,7 +1549,7 @@
2.91 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"
2.92 val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.93 term2str t;
2.94 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK*)
2.95 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK*)
2.96
2.97 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
2.98 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.99 @@ -1585,7 +1585,7 @@
2.100 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
2.101
2.102 (*Schalk I, p.69 Nr. 458b *)
2.103 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK
2.104 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK
2.105 val t = str2term
2.106 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
2.107 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.108 @@ -1608,7 +1608,7 @@
2.109
2.110
2.111 (*Schalk I, p.69 Nr. 460b *)
2.112 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK
2.113 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK
2.114 val t = str2term
2.115 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
2.116 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.117 @@ -1625,7 +1625,7 @@
2.118 "(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
2.119 val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.120 term2str t;
2.121 - ???SK*)
2.122 + ????SK*)
2.123
2.124 (*SRD Schalk I, p.70 Nr. 472a *)
2.125 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
2.126 @@ -1697,7 +1697,7 @@
2.127 (*----------------------------------------------------------------------*)
2.128
2.129 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
2.130 -(*WN060419 crashes with method 'simplify' ???SK*)
2.131 +(*WN060419 crashes with method 'simplify' ????SK*)
2.132 val t = str2term
2.133 "((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
2.134 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.135 @@ -1714,7 +1714,7 @@
2.136 \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
2.137 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.138 term2str t';
2.139 -if (term2str t') = ???SK ???MG
2.140 +if (term2str t') = ????SK ???MG
2.141
2.142 then ()
2.143 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 50";
2.144 @@ -1722,7 +1722,7 @@
2.145 val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / \
2.146 \((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
2.147 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.148 -term2str t; ???SK ???MG
2.149 +term2str t; ????SK ???MG
2.150 "(a ^^^ 2 * b ^^^ 4 * y + 2 * a ^^^ 2 * b ^^^ 3 * y ^^^ 2 +\n -4 * a ^^^ 2 * b ^^^ 2 * y ^^^ 3 +\n -8 * a ^^^ 2 * b * y ^^^ 4 +\n 4 * a * b ^^^ 4 * x * y +\n 8 * a * b ^^^ 3 * x * y ^^^ 2 +\n -16 * a * b ^^^ 2 * x * y ^^^ 3 +\n -32 * a * b * x * y ^^^ 4 +\n 4 * b ^^^ 4 * x ^^^ 2 * y +\n 8 * b ^^^ 3 * x ^^^ 2 * y ^^^ 2 +\n -16 * b ^^^ 2 * x ^^^ 2 * y ^^^ 3 +\n -32 * b * x ^^^ 2 * y ^^^ 4)
2.151 /\n(a ^^^ 2 * b ^^^ 5 * y + -1 * a ^^^ 2 * b ^^^ 4 * y ^^^ 2 +\n -3 * a ^^^ 2 * b ^^^ 3 * y ^^^ 3 +\n a ^^^ 2 * b ^^^ 2 * y ^^^ 4 +\n 2 * a ^^^ 2 * b * y ^^^ 5 +\n 2 * a * b ^^^ 5 * x * y +\n -2 * a * b ^^^ 4 * x * y ^^^ 2 +\n -6 * a * b ^^^ 3 * x * y ^^^ 3 +\n 2 * a * b ^^^ 2 * x * y ^^^ 4 +\n 4 * a * b * x * y ^^^ 5 +\n b ^^^ 5 * x ^^^ 2 * y +\n -1 * b ^^^ 4 * x ^^^ 2 * y ^^^ 2 +\n -3 * b ^^^ 3 * x ^^^ 2 * y ^^^ 3 +\n b ^^^ 2 * x ^^^ 2 * y ^^^ 4 +\n 2 * b * x ^^^ 2 * y ^^^ 5)";
2.152 *)
2.153 @@ -1733,7 +1733,7 @@
2.154 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.155 term2str t';
2.156 (* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
2.157 - ???SK ???MG
2.158 + ????SK ???MG
2.159 if term2str t' =
2.160 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
2.161 then ()
2.162 @@ -1741,7 +1741,7 @@
2.163 -----------------------------------------------------------------------*)
2.164
2.165 (*Schalk I, p.70 Nr. 480a *)
2.166 -(* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen: WN060831???SK00
2.167 +(* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen: WN060831????SK00
2.168 val t = str2term
2.169 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z) / (2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z)))";
2.170 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.171 @@ -1751,7 +1751,7 @@
2.172 then ()
2.173 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
2.174
2.175 -(*MG Berechne Zwischenergebnisse: WN060831???SK00*)
2.176 +(*MG Berechne Zwischenergebnisse: WN060831????SK00*)
2.177 val t = str2term
2.178 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
2.179 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.180 @@ -1777,7 +1777,7 @@
2.181 term2str t;
2.182 (*uncaught exception nonexhaustive binding failure*)
2.183
2.184 -(* Das kann er aber kürzen !!???: *)
2.185 +(* Das kann er aber kürzen !!????: *)
2.186 val t = str2term
2.187 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
2.188 val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.189 @@ -1885,56 +1885,29 @@
2.190 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
2.191 (*Eigenes*)
2.192 (* Achtung: Endlosschleife bei cancel_p:
2.193 -val t = str2term "(a^^^2 - 1)/(a+1)";
2.194 +val t = str2term "(a^^^2 + -1)/(a+1)";
2.195 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.196 term2str t;
2.197 "(-1 + a^^^2) / (1 + a)";
2.198 val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.199 term2str t;
2.200 "(-1 + 1 * a) / 1"; (*OK*)
2.201 -
2.202 -val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
2.203 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.204 -term2str t;
2.205 -"(-1 + -1 * b + a^^^2 + a^^^2 * b) /
2.206 -(-1 + -1 * a + b^^^2 + a * b^^^2)"
2.207 -val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.208 -term2str t;
2.209 -(* Endlosschleife*)
2.210 *)
2.211
2.212 +"----- NOT TERMINATING";
2.213 +val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
2.214 +val Some (t',_) = rewrite_set_ thy false make_polynomial t;
2.215 +term2str t' =
2.216 + "(-1 + -1 * b + a ^^^ 2 + a ^^^ 2 * b) /\n(-1 + -1 * a + b ^^^ 2 + a * b ^^^ 2)";
2.217 +(* NOT TERMINATING
2.218 +val Some (t'',_) = rewrite_set_ thy false cancel_p t';
2.219 +term2str t'';
2.220 + Endlosschleife*)
2.221
2.222 -
2.223 -
2.224 -
2.225 -(*--------------------------------------------------------------------*)
2.226 -(* EHEMALIG (MG 2004) FEHLER *)
2.227 -(*--------------------------------------------------------------------*)
2.228 -
2.229 -(* cancel_p liefert nicht immer Polynomnormalform (2):
2.230 - ---> Minus (binärer Operator) wird erzeugt !!! *)
2.231 -(*
2.232 -val t = str2term "-1 / (5 + -2 * x)";
2.233 -val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.234 -term2str t;
2.235 -"-1 / (5 - 2 * x)";*)
2.236 -(* ~~~ *)
2.237 -
2.238 -(*aber wenn im Zähler kein Minus tritt Problem nicht auf !!??:*)
2.239 -(*val t = str2term
2.240 -"1 / (5 + -2 * x)";
2.241 -val Some (t,_) = rewrite_set_ thy false cancel_p t;
2.242 -term2str t;
2.243 -"1 / (5 + -2 * x)";*)
2.244 -
2.245 -(* ACHTUNG: Endlosschleife !!! *)
2.246 -(*Schalk I, p.66 Nr. 381b *)
2.247 -(*val t = str2term
2.248 -"(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
2.249 -val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.250 -*)
2.251 -(*--------------------------------------------------------------------*)
2.252 -
2.253 +"----- corrected SK060905";
2.254 +val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
2.255 +val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
2.256 +term2str t' = "-1 / (5 + -2 * x)" (*true*);
2.257
2.258
2.259 "--------------------------------------------------------------------";
2.260 @@ -2120,30 +2093,25 @@
2.261 val Some (t', _) = cancel_p_ thy t; term2str t';
2.262 (*???SK order ???*)
2.263
2.264 -"----- SK060904-1a non-termination of cancel_p_";
2.265 +"----- SK060904-1a non-termination of cancel_p_ NOT CANCELED";
2.266 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
2.267 val Some (t',_) = rewrite_set_ thy false norm_Poly t;
2.268 term2str t' =
2.269 - "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true*);
2.270 -(* cancel_p_ thy t';
2.271 - Warning - Increasing stack from 147456 to 294912 bytes
2.272 - Warning - Increasing stack from 294912 to 589824 bytes
2.273 - Warning - Increasing stack from 589824 to 1179648 bytes*)
2.274 + "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true NOT CANCELED*);
2.275 +val Some (t'',_) = cancel_p_ thy t'; term2str t' =
2.276 +"(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true NOT CANCELED*);
2.277
2.278 -"----- SK060904-1b non-termination of cancel_p_";
2.279 +"----- SK060904-1b non-termination of cancel_p_ ... corrected";
2.280 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
2.281 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
2.282 -(* cancel_p_ thy t;
2.283 - Warning - Increasing stack from 147456 to 294912 bytes
2.284 - Warning - Increasing stack from 294912 to 589824 bytes
2.285 - Warning - Increasing stack from 589824 to 1179648 bytes*)
2.286 +val Some (t',_) = cancel_p_ thy t; term2str t' = "1 / (4 * c + 3 * e)"(*true*);
2.287
2.288
2.289 "----- SK060904-2a non-termination of add_fraction_p_";
2.290 val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \
2.291 \ (-1 * a + b * x) / (a + b * x) ";
2.292 (*
2.293 -rewrite_set_ thy false common_nominator_p t;
2.294 +val Some (t',_) = rewrite_set_ thy false common_nominator_p t;
2.295
2.296 common_nominator_p_ thy t;
2.297 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \