28 "-------- TODO ---------------------------------------------------------------"; |
28 "-------- TODO ---------------------------------------------------------------"; |
29 "-------- and app_rev --------------------------------------------------------"; |
29 "-------- and app_rev --------------------------------------------------------"; |
30 "-------- external calculating functions test -----------"; |
30 "-------- external calculating functions test -----------"; |
31 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; |
31 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; |
32 "-------- common_nominator_p ----------------------------"; |
32 "-------- common_nominator_p ----------------------------"; |
|
33 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
33 "-------- reverse rewrite -------------------------------"; |
34 "-------- reverse rewrite -------------------------------"; |
34 "-------- 'reverse-ruleset' cancel_p --------------------"; |
35 "-------- 'reverse-ruleset' cancel_p --------------------"; |
35 "-------- norm_Rational ---------------------------------"; |
36 "-------- norm_Rational ---------------------------------"; |
36 "-------- numeral rationals -----------------------------"; |
37 "-------- numeral rationals -----------------------------"; |
37 "-------- cancellation ----------------------------------"; |
38 "-------- cancellation ----------------------------------"; |
1057 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1058 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1058 val SOME (t',_) = factout_ thy t; |
1059 val SOME (t',_) = factout_ thy t; |
1059 if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then () |
1060 if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then () |
1060 else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1061 else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1061 |
1062 |
|
1063 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
|
1064 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
|
1065 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
|
1066 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)"); |
|
1067 "-------- gcd_poly integration level 1: works on exact term"; |
|
1068 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction"; |
|
1069 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction"; |
|
1070 |
|
1071 "-------- gcd_poly integration level 2: picks out ONE appropriate subterm"; |
|
1072 val SOME (t', asm) = rewrite_set_ thy false cancel_p t; |
|
1073 if term2str t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f" |
|
1074 then () else error "level 2, rewrite_set_ cancel_p: changed"; |
|
1075 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t; |
|
1076 if term2str t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)" |
|
1077 then () else error "level 2, rewrite_set_ add_fractions_p: changed"; |
|
1078 |
|
1079 "-------- gcd_poly integration level 3: rewrites all appropriate subterms"; |
|
1080 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t; |
|
1081 if term2str t' = "123 = a / b + c / d + e / f" |
|
1082 then () else error "level 3, rewrite_set_ cancel_p_rls: changed"; |
|
1083 val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*) |
|
1084 if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)" |
|
1085 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed"; |
|
1086 |
|
1087 "-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p"; |
|
1088 (* simpler variant *) |
|
1089 val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p] |
|
1090 val SOME (t', asm) = rewrite_set_ thy false testrls t; |
|
1091 (*trace_rewrite := false; |
|
1092 # rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) |
|
1093 ## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) |
|
1094 ## rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f |
|
1095 ## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f |
|
1096 ## rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f |
|
1097 ## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) |
|
1098 ## rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *) |
|
1099 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)" |
|
1100 then () else error "level 4, rewrite_set_ *_p: changed"; |
|
1101 |
|
1102 (* complicated variant *) |
|
1103 val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls]; |
|
1104 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t; |
|
1105 (*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) |
|
1106 ## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) |
|
1107 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) |
|
1108 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f |
|
1109 ### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f |
|
1110 ### rls: cancel_p on: 123 = a / b + c / d + e / f |
|
1111 ## rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f |
|
1112 ### rls: common_nominator_p on: 123 = a / b + c / d + e / f |
|
1113 ### rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f |
|
1114 ### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) |
|
1115 ## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) |
|
1116 ### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) |
|
1117 ## rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) |
|
1118 ### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *) |
|
1119 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)" |
|
1120 then () else error "level 4, rewrite_set_ *_p_rls: changed" |
|
1121 |
|
1122 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational"; |
|
1123 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t; |
|
1124 if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)" |
|
1125 then () else error "level 5, rewrite_set_ norm_Rational: changed" |
1062 |
1126 |
1063 "-------- reverse rewrite -------------------------------"; |
1127 "-------- reverse rewrite -------------------------------"; |
1064 "-------- reverse rewrite -------------------------------"; |
1128 "-------- reverse rewrite -------------------------------"; |
1065 "-------- reverse rewrite -------------------------------"; |
1129 "-------- reverse rewrite -------------------------------"; |
1066 (*WN.28.8.02: tests for the 'reverse-rewrite' functions: |
1130 (*WN.28.8.02: tests for the 'reverse-rewrite' functions: |