1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 14:10:45 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 15:50:33 2006 +0200
     1.3 @@ -495,11 +495,10 @@
     1.4  val Some (t,_) = rewrite_set thy' false "cancel" e188b';
     1.5  t = "5 / 6" (*true*);
     1.6  print("c)\n");
     1.7 -(*WN.23.10.02-------
     1.8 +
     1.9  val e188c'="( a + -1 * b ) / ( b + -1 * a )";
    1.10 -val e188c = the (rewrite_set thy' false "cancel" e188c');
    1.11 -  is_expanded (parse_rat "a + -1 * b");
    1.12 -  false; -----------!!! WN060831???SK5 geht am worksheet?!?*)
    1.13 +val e188c = the (rewrite_set thy' false "cancel_p" e188c');
    1.14 +(*is_expanded (parse_rat "a + -1 * b");*)
    1.15  val Some (t,_) = 
    1.16      rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
    1.17  if t= "(a + -1 * b) / (-1 * a + b)"  then()
    1.18 @@ -1506,6 +1505,7 @@
    1.19  then ()
    1.20  else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
    1.21  
    1.22 +
    1.23  (*Schalk I, p.69 Nr. 455b *)
    1.24  (* Achtung: Endlosschleife
    1.25  val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
    1.26 @@ -1516,6 +1516,7 @@
    1.27  then ()
    1.28  else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
    1.29  
    1.30 +
    1.31  val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
    1.32  val Some (t,_) = rewrite_set_ thy false make_polynomial t;
    1.33  term2str t;
    1.34 @@ -1528,14 +1529,14 @@
    1.35  val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
    1.36  val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
    1.37  term2str t;
    1.38 -(*ENDLOSSCHLEIFE!!! ???SK*)
    1.39 +(*ENDLOSSCHLEIFE!!! ???MG!!!*)
    1.40  
    1.41  val t = str2term "-1 / (3 + y)";
    1.42  (*                ~~         *)
    1.43  val Some (t,_) = rewrite_set_ thy false cancel_p t;
    1.44  term2str t = "-1 / (3 + 1 * y)";
    1.45  (********* Das ist das PROBLEM !!!!!!!??? *******************)
    1.46 -(*MG: -1 im Zähler der Angabe verursacht das Problem ! WN060831???SK0*)
    1.47 +(*MG: -1 im Zähler der Angabe verursacht das Problem ! WN060831???MG!!SK0*)
    1.48  *)
    1.49  
    1.50  (*SRD Schalk I, p.69 Nr. 456b *)
    1.51 @@ -1611,6 +1612,7 @@
    1.52  then ()
    1.53  else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
    1.54  
    1.55 +
    1.56  (*----------------------------------------------------------------------*)
    1.57  (*---------------------- Einfache Dppelbrüche --------------------------*)
    1.58  (*----------------------------------------------------------------------*)
    1.59 @@ -2079,6 +2081,7 @@
    1.60  "-------- SK 060904 ----------------------------------------------";
    1.61  "-------- SK 060904 ----------------------------------------------";
    1.62  "-------- SK 060904 ----------------------------------------------";
    1.63 +"----- order on polynomials -- input + output";
    1.64  val thy = Isac.thy;
    1.65  val t = str2term "(a + -1 * b) / (-1 * a + b)";
    1.66  val Some (t', _) = factout_p_ thy t; term2str t';
    1.67 @@ -2091,15 +2094,19 @@
    1.68  val Some (t', _) = cancel_p_ thy t; term2str t';
    1.69  (*???SK order ???*)
    1.70  
    1.71 -val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
    1.72 -val Some (t',_) = common_nominator_ thy t;
    1.73 -val Some (t'',_) = add_fraction_ thy t;
    1.74 +"----- non-termination of cancel_p_ S";
    1.75 +(*cancel_p_ does not terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.76 +val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
    1.77 +val Some (t',_) = rewrite_set_ thy false norm_Poly t; 
    1.78  term2str t' =
    1.79 -"(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x)) +\n1\
    1.80 -\ * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" (*true*);
    1.81 -term2str t'' = "(-1 - y - x) / (1 * y - x)" (*true*);
    1.82 -(*sometime before 060831???SK3..*)
    1.83 -"((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
    1.84 -\1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
    1.85 -(*sometime before 060831???SK3..*)"((-1) - y - x) / (y - x)";
    1.86 -(*WN.16.10.02             lexicographische Ordnung  ^^^^^^^ ?!*)
    1.87 +   "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true*);
    1.88 +(* cancel_p_ thy t'; 
    1.89 +   *)
    1.90 +
    1.91 +val mmm = (3,[2,1,1]);
    1.92 +fun mv_monom2str (i,is) = "("^int2str i^","^ints2str' is^")";
    1.93 +mv_monom2str mmm;
    1.94 +
    1.95 +val xxx = [(1,[1,0,0]),(2,[1,1,0]),(3,[2,1,1])];
    1.96 +fun mv_poly2str p = (strs2str' o (map mv_monom2str)) p;
    1.97 +mv_poly2str xxx;