1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 15:53:35 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 16:56:33 2006 +0200
     1.3 @@ -1020,10 +1020,12 @@
     1.4  (*WN.17.3.03 =========================================================^^^---*)
     1.5  
     1.6  
     1.7 +"----- SK060904-2a non-termination of add_fraction_p_";
     1.8  (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*)
     1.9  (*... takes uncredible much time:*)
    1.10  (*
    1.11  WN060831???SK6
    1.12 +"----- SK060904-2a non-termination of add_fraction_p_";
    1.13  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)";
    1.14  val None = rewrite_set_ thy false common_nominator_p t;
    1.15  writeln
    1.16 @@ -1332,6 +1334,7 @@
    1.17  val Some (t',_) = rewrite_set_ thy false make_polynomial t;
    1.18  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)";
    1.19  (*..WN060831 _with_ parentheses ...*)
    1.20 +"----- SK060904-1b non-termination of cancel_p_";
    1.21  val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
    1.22  \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
    1.23  (* WN060831???SK8
    1.24 @@ -1391,10 +1394,14 @@
    1.25  (* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831???SK11
    1.26  val t = str2term 
    1.27  "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
    1.28 +trace_rewrite := true;
    1.29  val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
    1.30 +###  rls: cancel_p on: 
    1.31 +(-9 * (a ^ 3 * b) + -9 * (a ^ 2 * b ^ 2) + a ^ 5 * b + a ^ 4 * b ^ 2) /
    1.32 +(3 * (a ^ 3 * b) + -3 * (a * b ^ 3) + a ^ 4 * b + -1 * (a ^ 2 * b ^ 3))
    1.33 +trace_rewrite := false;
    1.34  term2str t;
    1.35  if (term2str t) =
    1.36 -
    1.37  then ()
    1.38  else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27";
    1.39  
    1.40 @@ -1516,7 +1523,7 @@
    1.41  then ()
    1.42  else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
    1.43  
    1.44 -
    1.45 +"----- SK060904-1a non-termination of cancel_p_";
    1.46  val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
    1.47  val Some (t,_) = rewrite_set_ thy false make_polynomial t;
    1.48  term2str t;
    1.49 @@ -2094,17 +2101,36 @@
    1.50  val Some (t', _) = cancel_p_ thy t; term2str t';
    1.51  (*???SK order ???*)
    1.52  
    1.53 -"----- non-termination of cancel_p_ S";
    1.54 -(*cancel_p_ does not terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.55 -val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
    1.56 +"----- SK060904-1a non-termination of cancel_p_";
    1.57 +val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
    1.58  val Some (t',_) = rewrite_set_ thy false norm_Poly t; 
    1.59  term2str t' =
    1.60     "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true*);
    1.61  (* cancel_p_ thy t'; 
    1.62 -   *)
    1.63 +   Warning - Increasing stack from 147456 to 294912 bytes
    1.64 +   Warning - Increasing stack from 294912 to 589824 bytes
    1.65 +   Warning - Increasing stack from 589824 to 1179648 bytes*)
    1.66  
    1.67 -val mmm = (3,[2,1,1]);
    1.68 -mv_monom2str mmm;
    1.69 +"----- SK060904-1b non-termination of cancel_p_";
    1.70 +val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
    1.71 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
    1.72 +(* cancel_p_ thy t; 
    1.73 +   Warning - Increasing stack from 147456 to 294912 bytes
    1.74 +   Warning - Increasing stack from 294912 to 589824 bytes
    1.75 +   Warning - Increasing stack from 589824 to 1179648 bytes)
    1.76  
    1.77 -val xxx = [(1,[1,0,0]),(2,[1,1,0]),(3,[2,1,1])];
    1.78 -mv_poly2str xxx;
    1.79 +
    1.80 +"----- SK060904-2a non-termination of add_fraction_p_";
    1.81 +val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  \
    1.82 +		 \ (-1 * a + b * x) / (a + b * x)      ";
    1.83 +(*
    1.84 +rewrite_set_ thy false common_nominator_p t;
    1.85 +
    1.86 +common_nominator_p_ thy t;
    1.87 +" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) +  \
    1.88 +\ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
    1.89 +
    1.90 +add_fraction_p_ thy t; 
    1.91 +" ((a + b * x)*(a + b * x)  +  (-1 * a + b * x)*(a + -1 * (b * x))) /\
    1.92 +\ ((a + b * x)*(-1 * a + b * x))                                     ";
    1.93 +*)
    1.94 \ No newline at end of file