242 if p = ip andalso ip = ([], Res) then () |
242 if p = ip andalso ip = ([], Res) then () |
243 else error "autoCalculate for met_partial_fraction changed: final pos'"; |
243 else error "autoCalculate for met_partial_fraction changed: final pos'"; |
244 |
244 |
245 val (Form f, tac, asms) = pt_extract (pt, p); |
245 val (Form f, tac, asms) = pt_extract (pt, p); |
246 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso |
246 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso |
247 tac = NONE andalso |
|
248 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^ |
247 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^ |
249 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^ |
248 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^ |
250 "B is_polyexp,A is_polyexp," ^ |
249 "B is_polyexp,A is_polyexp," ^ |
251 "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^ |
250 "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^ |
252 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^ |
251 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^ |
253 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^ |
252 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^ |
254 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]" |
253 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]" |
255 then () |
254 then case tac of NONE => () |
256 else error "autoCalculate for met_partial_fraction changed: final result" |
255 | _ => error "autoCalculate for met_partial_fraction changed: final result 1" |
|
256 else error "autoCalculate for met_partial_fraction changed: final result 2" |
257 |
257 |
258 show_pt pt; |
258 show_pt pt; |
259 (*[ |
259 (*[ |
260 (([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])), |
260 (([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])), |
261 (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), |
261 (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), |