1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Sep 02 14:56:57 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Mon Sep 02 15:17:34 2013 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4  "-------- external calculating functions test -----------";
     1.5  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
     1.6  "-------- common_nominator_p ----------------------------";
     1.7 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
     1.8  "-------- reverse rewrite -------------------------------";
     1.9  "-------- 'reverse-ruleset' cancel_p --------------------";
    1.10  "-------- norm_Rational ---------------------------------";
    1.11 @@ -1059,6 +1060,69 @@
    1.12  if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then ()
    1.13  else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
    1.14      
    1.15 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
    1.16 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
    1.17 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
    1.18 +val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
    1.19 +"-------- gcd_poly integration level 1: works on exact term";
    1.20 +if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
    1.21 +if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";
    1.22 +
    1.23 +"-------- gcd_poly integration level 2: picks out ONE appropriate subterm";
    1.24 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
    1.25 +if term2str t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f" 
    1.26 +then () else error "level 2, rewrite_set_ cancel_p: changed";
    1.27 +val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t;
    1.28 +if term2str t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)"
    1.29 +then () else error "level 2, rewrite_set_ add_fractions_p: changed";
    1.30 +
    1.31 +"-------- gcd_poly integration level 3: rewrites all appropriate subterms";
    1.32 +val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
    1.33 +if term2str t' = "123 = a / b + c / d + e / f"
    1.34 +then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
    1.35 +val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*)
    1.36 +if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
    1.37 +then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
    1.38 +
    1.39 +"-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";
    1.40 +(* simpler variant *)
    1.41 +val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p]
    1.42 +val SOME (t', asm) = rewrite_set_ thy false testrls t;
    1.43 +(*trace_rewrite := false;
    1.44 +#  rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.45 +##  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.46 +##  rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f 
    1.47 +##  rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f 
    1.48 +##  rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f 
    1.49 +##  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) 
    1.50 +##  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
    1.51 +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
    1.52 +then () else error "level 4, rewrite_set_ *_p: changed";
    1.53 +
    1.54 +(* complicated variant *)
    1.55 +val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls];
    1.56 +val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
    1.57 +(*#  rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.58 +##  rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.59 +###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.60 +###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f 
    1.61 +###  rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f 
    1.62 +###  rls: cancel_p on: 123 = a / b + c / d + e / f 
    1.63 +##  rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f 
    1.64 +###  rls: common_nominator_p on: 123 = a / b + c / d + e / f 
    1.65 +###  rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f 
    1.66 +###  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) 
    1.67 +##  rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) 
    1.68 +###  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) 
    1.69 +##  rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) 
    1.70 +###  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
    1.71 +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
    1.72 +then () else error "level 4, rewrite_set_ *_p_rls: changed"
    1.73 +
    1.74 +"-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";
    1.75 +val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;
    1.76 +if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"
    1.77 +then () else error "level 5, rewrite_set_ norm_Rational: changed"
    1.78  
    1.79  "-------- reverse rewrite -------------------------------";
    1.80  "-------- reverse rewrite -------------------------------";