178 *) |
178 *) |
179 store_pbt |
179 store_pbt |
180 (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID |
180 (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID |
181 (["rational","univariate","equation"], |
181 (["rational","univariate","equation"], |
182 [("#Given" ,["equality e_e","solveFor v_v"]), |
182 [("#Given" ,["equality e_e","solveFor v_v"]), |
183 ("#Where" ,["(e_e::bool) is_ratequation_in (v_::real)"]), |
183 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
184 ("#Find" ,["solutions v_i"]) |
184 ("#Find" ,["solutions v_i"]) |
185 ], |
185 ], |
186 |
186 |
187 RatEq_prls, SOME "solve (e_e::bool, v_v)", |
187 RatEq_prls, SOME "solve (e_e::bool, v_v)", |
188 [["RatEq","solve_rat_equation"]])); |
188 [["RatEq","solve_rat_equation"]])); |
198 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
198 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
199 store_met |
199 store_met |
200 (prep_met thy "met_rat_eq" [] e_metID |
200 (prep_met thy "met_rat_eq" [] e_metID |
201 (["RatEq","solve_rat_equation"], |
201 (["RatEq","solve_rat_equation"], |
202 [("#Given" ,["equality e_e","solveFor v_v"]), |
202 [("#Given" ,["equality e_e","solveFor v_v"]), |
203 ("#Where" ,["(e_e::bool) is_ratequation_in (v_::real)"]), |
203 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
204 ("#Find" ,["solutions v_i"]) |
204 ("#Find" ,["solutions v_i"]) |
205 ], |
205 ], |
206 {rew_ord'="termlessI", |
206 {rew_ord'="termlessI", |
207 rls'=rateq_erls, |
207 rls'=rateq_erls, |
208 srls=e_rls, |
208 srls=e_rls, |
209 prls=RatEq_prls, |
209 prls=RatEq_prls, |
210 calc=[], |
210 calc=[], |
211 crls=RatEq_crls, nrls=norm_Rational}, |
211 crls=RatEq_crls, nrls=norm_Rational}, |
212 "Script Solve_rat_equation (e_e::bool) (v_::real) = " ^ |
212 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^ |
213 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^ |
213 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^ |
214 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^ |
214 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^ |
215 " (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ " ^ |
215 " (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ " ^ |
216 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_;" ^ |
216 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_;" ^ |
217 " (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], " ^ |
217 " (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], " ^ |
218 " [no_met]) [bool_ e_e, real_ v_]) " ^ |
218 " [no_met]) [bool_ e_e, real_ v_]) " ^ |
219 " in Check_elementwise L_ {(v_::real). Assumptions})" |
219 " in Check_elementwise L_ {(v_v::real). Assumptions})" |
220 )); |
220 )); |
221 |
221 |
222 calclist':= overwritel (!calclist', |
222 calclist':= overwritel (!calclist', |
223 [("is_ratequation_in", ("RatEq.is_ratequation_in", |
223 [("is_ratequation_in", ("RatEq.is_ratequation_in", |
224 eval_is_ratequation_in "")) |
224 eval_is_ratequation_in "")) |