36 fun fac_from_sol s = |
36 fun fac_from_sol s = |
37 let val (lhs, rhs) = HOLogic.dest_eq s |
37 let val (lhs, rhs) = HOLogic.dest_eq s |
38 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end; |
38 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end; |
39 |
39 |
40 fun mk_prod prod [] = |
40 fun mk_prod prod [] = |
41 if prod = e_term then error "mk_prod called with []" else prod |
41 if prod = Celem.e_term then error "mk_prod called with []" else prod |
42 | mk_prod prod (t :: []) = |
42 | mk_prod prod (t :: []) = |
43 if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t) |
43 if prod = Celem.e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t) |
44 | mk_prod prod (t1 :: t2 :: ts) = |
44 | mk_prod prod (t1 :: t2 :: ts) = |
45 if prod = e_term |
45 if prod = Celem.e_term |
46 then |
46 then |
47 let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2) |
47 let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2) |
48 in mk_prod p ts end |
48 in mk_prod p ts end |
49 else |
49 else |
50 let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1) |
50 let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1) |
51 in mk_prod p (t2 :: ts) end |
51 in mk_prod p (t2 :: ts) end |
52 |
52 |
53 fun factors_from_solution sol = |
53 fun factors_from_solution sol = |
54 let val ts = HOLogic.dest_list sol |
54 let val ts = HOLogic.dest_list sol |
55 in mk_prod e_term (map fac_from_sol ts) end; |
55 in mk_prod Celem.e_term (map fac_from_sol ts) end; |
56 |
56 |
57 (*("factors_from_solution", ("Partial_Fractions.factors_from_solution", |
57 (*("factors_from_solution", ("Partial_Fractions.factors_from_solution", |
58 eval_factors_from_solution ""))*) |
58 eval_factors_from_solution ""))*) |
59 fun eval_factors_from_solution (thmid:string) _ |
59 fun eval_factors_from_solution (thmid:string) _ |
60 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy = |
60 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy = |
61 ((let val prod = factors_from_solution sol |
61 ((let val prod = factors_from_solution sol |
62 in SOME (TermC.mk_thmid thmid (term_to_string''' thy prod) "", |
62 in SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy prod) "", |
63 HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) |
63 HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) |
64 end) |
64 end) |
65 handle _ => NONE) |
65 handle _ => NONE) |
66 | eval_factors_from_solution _ _ _ _ = NONE; |
66 | eval_factors_from_solution _ _ _ _ = NONE; |
67 *} |
67 *} |
123 TODOs for this version ar in partial_fractions.sml "--- progr.vers.2: " |
123 TODOs for this version ar in partial_fractions.sml "--- progr.vers.2: " |
124 *} |
124 *} |
125 |
125 |
126 ML {* |
126 ML {* |
127 val ansatz_rls = prep_rls'( |
127 val ansatz_rls = prep_rls'( |
128 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
128 Celem.Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord), |
129 erls = Erls, srls = Erls, calc = [], errpatts = [], |
129 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [], |
130 rules = |
130 rules = |
131 [Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}), |
131 [Celem.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}), |
132 Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order}) |
132 Celem.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order}) |
133 ], |
133 ], |
134 scr = EmptyScr}:rls); |
134 scr = Celem.EmptyScr}); |
135 |
135 |
136 val equival_trans = prep_rls'( |
136 val equival_trans = prep_rls'( |
137 Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
137 Celem.Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord), |
138 erls = Erls, srls = Erls, calc = [], errpatts = [], |
138 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [], |
139 rules = |
139 rules = |
140 [Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}), |
140 [Celem.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}), |
141 Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order}) |
141 Celem.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order}) |
142 ], |
142 ], |
143 scr = EmptyScr}:rls); |
143 scr = Celem.EmptyScr}); |
144 |
144 |
145 val multiply_ansatz = prep_rls'( |
145 val multiply_ansatz = prep_rls'( |
146 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
146 Celem.Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord), |
147 erls = Erls, |
147 erls = Celem.Erls, |
148 srls = Erls, calc = [], errpatts = [], |
148 srls = Celem.Erls, calc = [], errpatts = [], |
149 rules = |
149 rules = |
150 [Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order}) |
150 [Celem.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order}) |
151 ], |
151 ], |
152 scr = EmptyScr}:rls); |
152 scr = Celem.EmptyScr}); |
153 *} |
153 *} |
154 |
154 |
155 text {*store the rule set for math engine*} |
155 text {*store the rule set for math engine*} |
156 setup {* KEStore_Elems.add_rlss |
156 setup {* KEStore_Elems.add_rlss |
157 [("ansatz_rls", (Context.theory_name @{theory}, ansatz_rls)), |
157 [("ansatz_rls", (Context.theory_name @{theory}, ansatz_rls)), |
162 |
162 |
163 consts |
163 consts |
164 decomposedFunction :: "real => una" |
164 decomposedFunction :: "real => una" |
165 |
165 |
166 ML {* |
166 ML {* |
167 check_guhs_unique := false; (*WN120307 REMOVE after editing*) |
167 Celem.check_guhs_unique := false; (*WN120307 REMOVE after editing*) |
168 *} |
168 *} |
169 setup {* KEStore_Elems.add_pbts |
169 setup {* KEStore_Elems.add_pbts |
170 [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID |
170 [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Celem.e_pblID |
171 (["partial_fraction", "rational", "simplification"], |
171 (["partial_fraction", "rational", "simplification"], |
172 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
172 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
173 (* TODO: call this sub-problem with appropriate functionTerm: |
173 (* TODO: call this sub-problem with appropriate functionTerm: |
174 leading coefficient of the denominator is 1: to be checked here! and.. |
174 leading coefficient of the denominator is 1: to be checked here! and.. |
175 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
175 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
176 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
176 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
177 ("#Find" ,["decomposedFunction p_p'''"])], |
177 ("#Find" ,["decomposedFunction p_p'''"])], |
178 append_rls "e_rls" e_rls [(*for preds in where_ TODO*)], |
178 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_ TODO*)], |
179 NONE, |
179 NONE, |
180 [["simplification","of_rationals","to_partial_fraction"]]))] *} |
180 [["simplification","of_rationals","to_partial_fraction"]]))] *} |
181 |
181 |
182 subsection {* Method *} |
182 subsection {* Method *} |
183 consts |
183 consts |
184 PartFracScript :: "[real,real, real] => real" |
184 PartFracScript :: "[real,real, real] => real" |
185 ("((Script PartFracScript (_ _ =))// (_))" 9) |
185 ("((Script PartFracScript (_ _ =))// (_))" 9) |
186 |
186 |
187 text {* rule set for functions called in the Script *} |
187 text {* rule set for functions called in the Script *} |
188 ML {* |
188 ML {* |
189 val srls_partial_fraction = Rls {id="srls_partial_fraction", |
189 val srls_partial_fraction = Celem.Rls {id="srls_partial_fraction", |
190 preconds = [], |
190 preconds = [], |
191 rew_ord = ("termlessI",termlessI), |
191 rew_ord = ("termlessI",termlessI), |
192 erls = append_rls "erls_in_srls_partial_fraction" e_rls |
192 erls = Celem.append_rls "erls_in_srls_partial_fraction" Celem.e_rls |
193 [(*for asm in NTH_CONS ...*) |
193 [(*for asm in NTH_CONS ...*) |
194 Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
194 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
195 (*2nd NTH_CONS pushes n+-1 into asms*) |
195 (*2nd NTH_CONS pushes n+-1 into asms*) |
196 Calc("Groups.plus_class.plus", eval_binop "#add_")], |
196 Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")], |
197 srls = Erls, calc = [], errpatts = [], |
197 srls = Celem.Erls, calc = [], errpatts = [], |
198 rules = [ |
198 rules = [ |
199 Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
199 Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
200 Calc("Groups.plus_class.plus", eval_binop "#add_"), |
200 Celem.Calc("Groups.plus_class.plus", eval_binop "#add_"), |
201 Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
201 Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
202 Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
202 Celem.Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
203 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
203 Celem.Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
204 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), |
204 Celem.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), |
205 Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), |
205 Celem.Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), |
206 Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
206 Celem.Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
207 Calc("Partial_Fractions.factors_from_solution", |
207 Celem.Calc("Partial_Fractions.factors_from_solution", |
208 eval_factors_from_solution "#factors_from_solution"), |
208 eval_factors_from_solution "#factors_from_solution"), |
209 Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")], |
209 Celem.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")], |
210 scr = EmptyScr}; |
210 scr = Celem.EmptyScr}; |
211 *} |
211 *} |
212 ML {* |
212 ML {* |
213 eval_drop_questionmarks; |
213 eval_drop_questionmarks; |
214 *} |
214 *} |
215 ML {* |
215 ML {* |
221 TermC.parseNEW ctxt "decomposedFunction"; |
221 TermC.parseNEW ctxt "decomposedFunction"; |
222 *} |
222 *} |
223 |
223 |
224 (* current version, error outcommented *) |
224 (* current version, error outcommented *) |
225 setup {* KEStore_Elems.add_mets |
225 setup {* KEStore_Elems.add_mets |
226 [Specify.prep_met @{theory} "met_partial_fraction" [] e_metID |
226 [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID |
227 (["simplification","of_rationals","to_partial_fraction"], |
227 (["simplification","of_rationals","to_partial_fraction"], |
228 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
228 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
229 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
229 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < |
230 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
230 ((get_denominator t_t) has_degree_in v_v)"]), TODO*) |
231 ("#Find" ,["decomposedFunction p_p'''"])], |
231 ("#Find" ,["decomposedFunction p_p'''"])], |
232 (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
232 (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
233 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls, |
233 {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = srls_partial_fraction, prls = Celem.e_rls, |
234 crls = e_rls, errpats = [], nrls = e_rls}, |
234 crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls}, |
235 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*) |
235 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*) |
236 "Script PartFracScript (f_f::real) (zzz::real) = " ^ |
236 "Script PartFracScript (f_f::real) (zzz::real) = " ^ |
237 (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
237 (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
238 "(let f_f = Take f_f; " ^ |
238 "(let f_f = Take f_f; " ^ |
239 (* num_orig = 3*) |
239 (* num_orig = 3*) |