272 " (pbz::real) = Take eqr; " ^(*([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*) |
272 " (pbz::real) = Take eqr; " ^(*([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*) |
273 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
273 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
274 "in pbz)" (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
274 "in pbz)" (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
275 )); |
275 )); |
276 *} |
276 *} |
|
277 setup {* KEStore_Elems.add_mets |
|
278 [prep_met @{theory} "met_partial_fraction" [] e_metID |
|
279 (["simplification","of_rationals","to_partial_fraction"], |
|
280 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
|
281 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
|
282 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
|
283 ("#Find" ,["decomposedFunction p_p'''"])], |
|
284 (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
|
285 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls, |
|
286 crls = e_rls, errpats = [], nrls = e_rls}, |
|
287 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*) |
|
288 "Script PartFracScript (f_f::real) (zzz::real) = " ^ |
|
289 (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
|
290 "(let f_f = Take f_f; " ^ |
|
291 (* num_orig = 3*) |
|
292 " (num_orig::real) = get_numerator f_f; " ^ |
|
293 (*([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)*) |
|
294 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^ |
|
295 (* denom = -1 + -2 * z + 8 * z ^^^ 2*) |
|
296 " (denom::real) = get_denominator f_f; " ^ |
|
297 (* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*) |
|
298 " (equ::bool) = (denom = (0::real)); " ^ |
|
299 |
|
300 (*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*) |
|
301 " (L_L::bool list) = (SubProblem (PolyEq', " ^ |
|
302 " [abcFormula, degree_2, polynomial, univariate, equation], " ^ |
|
303 (*([2], Res), [z = 1 / 2, z = -1 / 4]*) |
|
304 " [no_met]) [BOOL equ, REAL zzz]); " ^ |
|
305 (* facs: (z - 1 / 2) * (z - -1 / 4)*) |
|
306 " (facs::real) = factors_from_solution L_L; " ^ |
|
307 (*([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4)) *) |
|
308 " (eql::real) = Take (num_orig / facs); " ^ |
|
309 (*([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*) |
|
310 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^ |
|
311 (*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*) |
|
312 " (eq::bool) = Take (eql = eqr); " ^ |
|
313 (*([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*) |
|
314 " eq = (Try (Rewrite_Set equival_trans False)) eq;" ^ |
|
315 (* eq = 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
316 " eq = drop_questionmarks eq; " ^ |
|
317 (* z1 = 1 / 2*) |
|
318 " (z1::real) = (rhs (NTH 1 L_L)); " ^ |
|
319 (* z2 = -1 / 4*) |
|
320 " (z2::real) = (rhs (NTH 2 L_L)); " ^ |
|
321 (*([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
322 " (eq_a::bool) = Take eq; " ^ |
|
323 (*([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*) |
|
324 " eq_a = (Substitute [zzz = z1]) eq; " ^ |
|
325 (*([6], Res), 3 = 3 * A / 4*) |
|
326 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^ |
|
327 |
|
328 (*([7], Pbl), solve (3 = 3 * A / 4, A)*) |
|
329 " (sol_a::bool list) = " ^ |
|
330 " (SubProblem (Isac', [univariate,equation], [no_met]) " ^ |
|
331 (*([7], Res), [A = 4]*) |
|
332 " [BOOL eq_a, REAL (A::real)]); " ^ |
|
333 (* a = 4*) |
|
334 " (a::real) = (rhs (NTH 1 sol_a)); " ^ |
|
335 (*([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
336 " (eq_b::bool) = Take eq; " ^ |
|
337 (*([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)*) |
|
338 " eq_b = (Substitute [zzz = z2]) eq_b; " ^ |
|
339 (*([9], Res), 3 = -3 * B / 4*) |
|
340 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^ |
|
341 (*([10], Pbl), solve (3 = -3 * B / 4, B)*) |
|
342 " (sol_b::bool list) = " ^ |
|
343 " (SubProblem (Isac', [univariate,equation], [no_met]) " ^ |
|
344 (*([10], Res), [B = -4]*) |
|
345 " [BOOL eq_b, REAL (B::real)]); " ^ |
|
346 (* b = -4*) |
|
347 " (b::real) = (rhs (NTH 1 sol_b)); " ^ |
|
348 (* eqr = A / (z - 1 / 2) + B / (z - -1 / 4)*) |
|
349 " eqr = drop_questionmarks eqr; " ^ |
|
350 (*([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*) |
|
351 " (pbz::real) = Take eqr; " ^ |
|
352 (*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
353 " pbz = ((Substitute [A = a, B = b]) pbz) " ^ |
|
354 (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
355 "in pbz)" |
|
356 )] |
|
357 *} |
277 ML {* |
358 ML {* |
278 (* |
359 (* |
279 val fmz = |
360 val fmz = |
280 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", |
361 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", |
281 "solveFor z", "functionTerm p_p"]; |
362 "solveFor z", "functionTerm p_p"]; |