873 rat_mult_poly = rat_mult_poly and |
873 rat_mult_poly = rat_mult_poly and |
874 rat_mult_div_pow = rat_mult_div_pow and |
874 rat_mult_div_pow = rat_mult_div_pow and |
875 cancel_p_rls = cancel_p_rls |
875 cancel_p_rls = cancel_p_rls |
876 |
876 |
877 section \<open>A problem for simplification of rationals\<close> |
877 section \<open>A problem for simplification of rationals\<close> |
878 setup \<open>KEStore_Elems.add_pbts |
878 |
879 [(Problem.prep_input @{theory} "pbl_simp_rat" [] Problem.id_empty |
879 problem pbl_simp_rat : "rational/simplification" = |
880 (["rational", "simplification"], |
880 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close> |
881 [("#Given" ,["Term t_t"]), |
881 Method: "simplification/of_rationals" |
882 ("#Where" ,["t_t is_ratpolyexp"]), |
882 CAS: "Simplify t_t" |
883 ("#Find" ,["normalform n_n"])], |
883 Given: "Term t_t" |
884 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], |
884 Where: "t_t is_ratpolyexp" |
885 SOME "Simplify t_t", [["simplification", "of_rationals"]]))]\<close> |
885 Find: "normalform n_n" |
886 |
886 |
887 section \<open>A methods for simplification of rationals\<close> |
887 section \<open>A methods for simplification of rationals\<close> |
888 (*WN061025 this methods script is copied from (auto-generated) script |
888 (*WN061025 this methods script is copied from (auto-generated) script |
889 of norm_Rational in order to ease repair on inform*) |
889 of norm_Rational in order to ease repair on inform*) |
890 |
890 |