104 TODOs for this version are in partial_fractions.sml "--- progr.vers.2: " |
104 TODOs for this version are in partial_fractions.sml "--- progr.vers.2: " |
105 \<close> |
105 \<close> |
106 |
106 |
107 ML \<open> |
107 ML \<open> |
108 val ansatz_rls = prep_rls'( |
108 val ansatz_rls = prep_rls'( |
109 Rule.Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
109 Rule_Set.Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
110 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], |
110 erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [], |
111 rules = |
111 rules = |
112 [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}), |
112 [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}), |
113 Rule.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order}) |
113 Rule.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order}) |
114 ], |
114 ], |
115 scr = Rule.EmptyScr}); |
115 scr = Rule.EmptyScr}); |
116 |
116 |
117 val equival_trans = prep_rls'( |
117 val equival_trans = prep_rls'( |
118 Rule.Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
118 Rule_Set.Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
119 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], |
119 erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [], |
120 rules = |
120 rules = |
121 [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}), |
121 [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}), |
122 Rule.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order}) |
122 Rule.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order}) |
123 ], |
123 ], |
124 scr = Rule.EmptyScr}); |
124 scr = Rule.EmptyScr}); |
125 |
125 |
126 val multiply_ansatz = prep_rls'( |
126 val multiply_ansatz = prep_rls'( |
127 Rule.Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
127 Rule_Set.Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), |
128 erls = Rule.Erls, |
128 erls = Rule_Set.Erls, |
129 srls = Rule.Erls, calc = [], errpatts = [], |
129 srls = Rule_Set.Erls, calc = [], errpatts = [], |
130 rules = |
130 rules = |
131 [Rule.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order}) |
131 [Rule.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order}) |
132 ], |
132 ], |
133 scr = Rule.EmptyScr}); |
133 scr = Rule.EmptyScr}); |
134 \<close> |
134 \<close> |
154 (* TODO: call this sub-problem with appropriate functionTerm: |
154 (* TODO: call this sub-problem with appropriate functionTerm: |
155 leading coefficient of the denominator is 1: to be checked here! and.. |
155 leading coefficient of the denominator is 1: to be checked here! and.. |
156 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
156 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
157 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
157 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
158 ("#Find" ,["decomposedFunction p_p'''"])], |
158 ("#Find" ,["decomposedFunction p_p'''"])], |
159 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_ TODO*)], |
159 Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_ TODO*)], |
160 NONE, |
160 NONE, |
161 [["simplification","of_rationals","to_partial_fraction"]]))]\<close> |
161 [["simplification","of_rationals","to_partial_fraction"]]))]\<close> |
162 |
162 |
163 subsection \<open>Method\<close> |
163 subsection \<open>Method\<close> |
164 text \<open>rule set for functions called in the Program\<close> |
164 text \<open>rule set for functions called in the Program\<close> |
165 ML \<open> |
165 ML \<open> |
166 val srls_partial_fraction = Rule.Rls {id="srls_partial_fraction", |
166 val srls_partial_fraction = Rule_Set.Rls {id="srls_partial_fraction", |
167 preconds = [], |
167 preconds = [], |
168 rew_ord = ("termlessI",termlessI), |
168 rew_ord = ("termlessI",termlessI), |
169 erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls |
169 erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls |
170 [(*for asm in NTH_CONS ...*) |
170 [(*for asm in NTH_CONS ...*) |
171 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
171 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
172 (*2nd NTH_CONS pushes n+-1 into asms*) |
172 (*2nd NTH_CONS pushes n+-1 into asms*) |
173 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], |
173 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], |
174 srls = Rule.Erls, calc = [], errpatts = [], |
174 srls = Rule_Set.Erls, calc = [], errpatts = [], |
175 rules = [ |
175 rules = [ |
176 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
176 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
177 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
177 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
178 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
178 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
179 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
179 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
233 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
233 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
234 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
234 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
235 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
235 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
236 ("#Find" ,["decomposedFunction p_p'''"])], |
236 ("#Find" ,["decomposedFunction p_p'''"])], |
237 (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
237 (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
238 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls, |
238 {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule_Set.e_rls, |
239 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, |
239 crls = Rule_Set.e_rls, errpats = [], nrls = Rule_Set.e_rls}, |
240 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*) |
240 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*) |
241 @{thm partial_fraction.simps})] |
241 @{thm partial_fraction.simps})] |
242 \<close> |
242 \<close> |
243 ML \<open> |
243 ML \<open> |
244 (* |
244 (* |