892 ("#Find" ,["normalform n_n"])], |
892 ("#Find" ,["normalform n_n"])], |
893 append_rls "e_rls" e_rls [(*for preds in where_*)], |
893 append_rls "e_rls" e_rls [(*for preds in where_*)], |
894 SOME "Simplify t_t", [["simplification","of_rationals"]]))] *} |
894 SOME "Simplify t_t", [["simplification","of_rationals"]]))] *} |
895 |
895 |
896 section {* A methods for simplification of rationals *} |
896 section {* A methods for simplification of rationals *} |
897 ML {* |
|
898 (*WN061025 this methods script is copied from (auto-generated) script |
|
899 of norm_Rational in order to ease repair on inform*) |
|
900 store_met (prep_met thy "met_simp_rat" [] e_metID (["simplification","of_rationals"], |
|
901 [("#Given" ,["Term t_t"]), |
|
902 ("#Where" ,["t_t is_ratpolyexp"]), |
|
903 ("#Find" ,["normalform n_n"])], |
|
904 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
905 prls = append_rls "simplification_of_rationals_prls" e_rls |
|
906 [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], |
|
907 crls = e_rls, errpats = [], |
|
908 nrls = norm_Rational_rls}, |
|
909 "Script SimplifyScript (t_t::real) = " ^ |
|
910 " ((Try (Rewrite_Set discard_minus False) @@ " ^ |
|
911 " Try (Rewrite_Set rat_mult_poly False) @@ " ^ |
|
912 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^ |
|
913 " Try (Rewrite_Set cancel_p_rls False) @@ " ^ |
|
914 " (Repeat " ^ |
|
915 " ((Try (Rewrite_Set add_fractions_p_rls False) @@ " ^ |
|
916 " Try (Rewrite_Set rat_mult_div_pow False) @@ " ^ |
|
917 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^ |
|
918 " Try (Rewrite_Set cancel_p_rls False) @@ " ^ |
|
919 " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^ |
|
920 " Try (Rewrite_Set discard_parentheses1 False)) " ^ |
|
921 " t_t)")); |
|
922 *} |
|
923 (*WN061025 this methods script is copied from (auto-generated) script |
897 (*WN061025 this methods script is copied from (auto-generated) script |
924 of norm_Rational in order to ease repair on inform*) |
898 of norm_Rational in order to ease repair on inform*) |
925 setup {* KEStore_Elems.add_mets |
899 setup {* KEStore_Elems.add_mets |
926 [prep_met thy "met_simp_rat" [] e_metID |
900 [prep_met thy "met_simp_rat" [] e_metID |
927 (["simplification","of_rationals"], |
901 (["simplification","of_rationals"], |