445 let |
446 let |
446 val vs = t |> vars |> map free2str |> sort string_ord |
447 val vs = t |> vars |> map free2str |> sort string_ord |
447 val baseT = type_of n1 |
448 val baseT = type_of n1 |
448 val expT = HOLogic.realT |
449 val expT = HOLogic.realT |
449 in |
450 in |
450 case (poly_of_term vs d1, poly_of_term vs d2) of |
451 (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of |
451 (SOME a, SOME b) => |
452 (SOME _, SOME a, SOME _, SOME b) => |
452 let |
453 let |
453 val ((a', b'), c) = gcd_poly a b |
454 val ((a', b'), c) = gcd_poly a b |
454 val nomin = term_of_poly baseT expT vs |
455 val nomin = term_of_poly baseT expT vs |
455 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) |
456 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) |
456 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b') |
457 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b') |
3568 (*FIXME.WN0401 ? redesign Rrls - use exhaustively on a term ? |
3569 (*FIXME.WN0401 ? redesign Rrls - use exhaustively on a term ? |
3569 FIXME.WN0510 unnecessary nesting: introduce RRls_ : rls -> rule*) |
3570 FIXME.WN0510 unnecessary nesting: introduce RRls_ : rls -> rule*) |
3570 ], |
3571 ], |
3571 scr = EmptyScr}); |
3572 scr = EmptyScr}); |
3572 (* ------------------------------------------------------------------- *) |
3573 (* ------------------------------------------------------------------- *) |
|
3574 (* "Rls" causes repeated application of cancel_p to one and the same term *) |
3573 val cancel_p_rls = prep_rls( |
3575 val cancel_p_rls = prep_rls( |
3574 Rls {id = "cancel_p_rls", preconds = [], |
3576 Rls |
3575 rew_ord = ("dummy_ord",dummy_ord), |
3577 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), |
3576 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
3578 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
3577 rules = |
3579 rules = |
3578 [Rls_ cancel_p |
3580 [Rls_ cancel_p (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*) |
3579 (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*) |
3581 ], |
3580 ], |
3582 scr = EmptyScr}); |
3581 scr = EmptyScr}); |
|
3582 (* -------------------------------------------------------------------- *) |
3583 (* -------------------------------------------------------------------- *) |
3583 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
3584 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
3584 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*) |
3585 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*) |
3585 val rat_mult_poly = prep_rls( |
3586 val rat_mult_poly = prep_rls( |
3586 Rls {id = "rat_mult_poly", preconds = [], |
3587 Rls {id = "rat_mult_poly", preconds = [], |
3659 ], |
3660 ], |
3660 scr = EmptyScr}:rls); |
3661 scr = EmptyScr}:rls); |
3661 (* ------------------------------------------------------------------ *) |
3662 (* ------------------------------------------------------------------ *) |
3662 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG) |
3663 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG) |
3663 just be renaming:*) |
3664 just be renaming:*) |
3664 val norm_Rational(*_mg*) = prep_rls( |
3665 val norm_Rational (*_mg*) = prep_rls( |
3665 Seq {id = "norm_Rational"(*_mg*), preconds = [], |
3666 Seq |
3666 rew_ord = ("dummy_ord",dummy_ord), |
3667 {id = "norm_Rational"(*_mg*), preconds = [], |
3667 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], |
3668 rew_ord = ("dummy_ord",dummy_ord), |
3668 rules = [Rls_ discard_minus, |
3669 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], |
3669 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
3670 rules = [Rls_ discard_minus, |
3670 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
3671 Rls_ rat_mult_poly, (* removes double fractions like a/b/c *) |
3671 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
3672 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
3672 Rls_ norm_Rational_rls, (* the main rls, looping (#) *) |
3673 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
3673 Rls_ discard_parentheses1 (* mult only *) |
3674 Rls_ norm_Rational_rls, (* the main rls, looping (#) *) |
3674 ], |
3675 Rls_ discard_parentheses1 (* mult only *) |
3675 scr = EmptyScr}:rls); |
3676 ], |
|
3677 scr = EmptyScr}:rls); |
|
3678 "-------- rls norm_Rational --------------------------------------------------"; |
3676 (* ------------------------------------------------------------------ *) |
3679 (* ------------------------------------------------------------------ *) |
3677 |
3680 |
3678 *} |
3681 *} |
3679 ML {* |
3682 ML {* |
3680 ruleset' := overwritelthy @{theory} (!ruleset', |
3683 ruleset' := overwritelthy @{theory} (!ruleset', |