106 |
106 |
107 ML \<open> |
107 ML \<open> |
108 val ansatz_rls = prep_rls'( |
108 val ansatz_rls = prep_rls'( |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
111 rules = |
111 rules = [ |
112 [\<^rule_thm>\<open>ansatz_2nd_order\<close>, |
112 \<^rule_thm>\<open>ansatz_2nd_order\<close>, |
113 \<^rule_thm>\<open>ansatz_3rd_order\<close> |
113 \<^rule_thm>\<open>ansatz_3rd_order\<close>], |
114 ], |
114 scr = Rule.Empty_Prog}); |
115 scr = Rule.Empty_Prog}); |
|
116 |
115 |
117 val equival_trans = prep_rls'( |
116 val equival_trans = prep_rls'( |
118 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
117 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
119 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
118 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
120 rules = |
119 rules = [ |
121 [\<^rule_thm>\<open>equival_trans_2nd_order\<close>, |
120 \<^rule_thm>\<open>equival_trans_2nd_order\<close>, |
122 \<^rule_thm>\<open>equival_trans_3rd_order\<close> |
121 \<^rule_thm>\<open>equival_trans_3rd_order\<close>], |
123 ], |
122 scr = Rule.Empty_Prog}); |
124 scr = Rule.Empty_Prog}); |
|
125 |
123 |
126 val multiply_ansatz = prep_rls'( |
124 val multiply_ansatz = prep_rls'( |
127 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
125 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
128 erls = Rule_Set.Empty, |
126 erls = Rule_Set.Empty, |
129 srls = Rule_Set.Empty, calc = [], errpatts = [], |
127 srls = Rule_Set.Empty, calc = [], errpatts = [], |
130 rules = |
128 rules = [ |
131 [\<^rule_thm>\<open>multiply_2nd_order\<close> |
129 \<^rule_thm>\<open>multiply_2nd_order\<close>], |
132 ], |
130 scr = Rule.Empty_Prog}); |
133 scr = Rule.Empty_Prog}); |
|
134 \<close> |
131 \<close> |
135 |
132 |
136 text \<open>store the rule set for math engine\<close> |
133 text \<open>store the rule set for math engine\<close> |
137 rule_set_knowledge |
134 rule_set_knowledge |
138 ansatz_rls = ansatz_rls and |
135 ansatz_rls = ansatz_rls and |
158 Find: "decomposedFunction p_p'''" |
155 Find: "decomposedFunction p_p'''" |
159 |
156 |
160 subsection \<open>MethodC\<close> |
157 subsection \<open>MethodC\<close> |
161 text \<open>rule set for functions called in the Program\<close> |
158 text \<open>rule set for functions called in the Program\<close> |
162 ML \<open> |
159 ML \<open> |
163 val srls_partial_fraction = Rule_Def.Repeat {id="srls_partial_fraction", |
160 val srls_partial_fraction = Rule_Def.Repeat {id="srls_partial_fraction", |
164 preconds = [], |
161 preconds = [], |
165 rew_ord = ("termlessI",termlessI), |
162 rew_ord = ("termlessI",termlessI), |
166 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty |
163 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty |
167 [(*for asm in NTH_CONS ...*) |
164 [(*for asm in NTH_CONS ...*) |
168 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
165 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
169 (*2nd NTH_CONS pushes n+-1 into asms*) |
166 (*2nd NTH_CONS pushes n+-1 into asms*) |
170 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
167 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
171 srls = Rule_Set.Empty, calc = [], errpatts = [], |
168 srls = Rule_Set.Empty, calc = [], errpatts = [], |
172 rules = [ |
169 rules = [ |
173 \<^rule_thm>\<open>NTH_CONS\<close>, |
170 \<^rule_thm>\<open>NTH_CONS\<close>, |
174 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
171 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
175 \<^rule_thm>\<open>NTH_NIL\<close>, |
172 \<^rule_thm>\<open>NTH_NIL\<close>, |
176 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
173 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
177 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
174 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
178 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
175 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
179 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |
176 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |
180 \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"), |
177 \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"), |
181 \<^rule_eval>\<open>factors_from_solution\<close> |
178 \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")], |
182 (eval_factors_from_solution "#factors_from_solution") |
179 scr = Rule.Empty_Prog}; |
183 ], |
|
184 scr = Rule.Empty_Prog}; |
|
185 \<close> |
180 \<close> |
186 |
181 |
187 (* current version, error outcommented *) |
182 (* current version, error outcommented *) |
188 partial_function (tailrec) partial_fraction :: "real \<Rightarrow> real \<Rightarrow> real" |
183 partial_function (tailrec) partial_fraction :: "real \<Rightarrow> real \<Rightarrow> real" |
189 where |
184 where |