168 ("#Find", ["solutions v_v'i'"])], |
168 ("#Find", ["solutions v_v'i'"])], |
169 RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq", "solve_rat_equation"]]))]\<close> |
169 RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq", "solve_rat_equation"]]))]\<close> |
170 |
170 |
171 subsection \<open>methods\<close> |
171 subsection \<open>methods\<close> |
172 setup \<open>KEStore_Elems.add_mets |
172 setup \<open>KEStore_Elems.add_mets |
173 [Method.prep_input thy "met_rateq" [] Method.id_empty |
173 [MethodC.prep_input thy "met_rateq" [] MethodC.id_empty |
174 (["RatEq"], [], |
174 (["RatEq"], [], |
175 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
175 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
176 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close> |
176 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close> |
177 |
177 |
178 partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
178 partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
186 (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e; |
186 (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e; |
187 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v] |
187 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v] |
188 in |
188 in |
189 Check_elementwise L_L {(v_v::real). Assumptions})" |
189 Check_elementwise L_L {(v_v::real). Assumptions})" |
190 setup \<open>KEStore_Elems.add_mets |
190 setup \<open>KEStore_Elems.add_mets |
191 [Method.prep_input thy "met_rat_eq" [] Method.id_empty |
191 [MethodC.prep_input thy "met_rat_eq" [] MethodC.id_empty |
192 (["RatEq", "solve_rat_equation"], |
192 (["RatEq", "solve_rat_equation"], |
193 [("#Given" ,["equality e_e", "solveFor v_v"]), |
193 [("#Given" ,["equality e_e", "solveFor v_v"]), |
194 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
194 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
195 ("#Find" ,["solutions v_v'i'"])], |
195 ("#Find" ,["solutions v_v'i'"])], |
196 {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule_Set.empty, prls=RatEq_prls, calc=[], |
196 {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule_Set.empty, prls=RatEq_prls, calc=[], |