514 val cancel_p = |
514 val cancel_p = |
515 Rule_Set.Rrls {id = "cancel_p", prepat = [], |
515 Rule_Set.Rrls {id = "cancel_p", prepat = [], |
516 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
516 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
517 erls = rational_erls, |
517 erls = rational_erls, |
518 calc = |
518 calc = |
519 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
519 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), |
520 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
520 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")), |
521 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
521 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
522 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))], |
522 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))], |
523 errpatts = [], |
523 errpatts = [], |
524 scr = |
524 scr = |
525 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro, |
525 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro, |
526 normal_form = cancel_p_ \<^theory>, |
526 normal_form = cancel_p_ \<^theory>, |
527 locate_rule = locate_rule \<^theory> Atools_erls ro, |
527 locate_rule = locate_rule \<^theory> Atools_erls ro, |
581 |
581 |
582 val add_fractions_p = |
582 val add_fractions_p = |
583 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat, |
583 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat, |
584 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
584 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
585 erls = rational_erls, |
585 erls = rational_erls, |
586 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
586 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), |
587 ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
587 ("TIMES", (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")), |
588 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
588 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
589 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))], |
589 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))], |
590 errpatts = [], |
590 errpatts = [], |
591 scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro, |
591 scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro, |
592 normal_form = add_fraction_p_ \<^theory>, |
592 normal_form = add_fraction_p_ \<^theory>, |
593 locate_rule = locate_rule \<^theory> Atools_erls ro, |
593 locate_rule = locate_rule \<^theory> Atools_erls ro, |
594 next_rule = next_rule \<^theory> Atools_erls ro, |
594 next_rule = next_rule \<^theory> Atools_erls ro, |
621 \<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*) |
621 \<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*) |
622 |
622 |
623 (*----- distribute none-atoms -----*) |
623 (*----- distribute none-atoms -----*) |
624 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*) |
624 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*) |
625 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*) |
625 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*) |
626 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
626 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], |
627 scr = Rule.Empty_Prog}); |
627 scr = Rule.Empty_Prog}); |
628 |
628 |
629 \<close> ML \<open> |
629 \<close> ML \<open> |
630 (*.contains absolute minimum of thms for context in norm_Rational.*) |
630 (*.contains absolute minimum of thms for context in norm_Rational.*) |
631 val rat_mult_divide = prep_rls'( |
631 val rat_mult_divide = prep_rls'( |