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" |
179 where |
179 where |
180 "solve_rational_equ e_e v_v = |
180 "solve_rational_equ e_e v_v = |
181 (let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@ |
181 (let |
182 (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@ |
182 e_e = ( |
183 (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@ |
183 (Repeat (Try (Rewrite_Set ''RatEq_simplify''))) @@ |
184 (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e; |
184 (Repeat (Try (Rewrite_Set ''norm_Rational''))) @@ |
185 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) |
185 (Repeat (Try (Rewrite_Set ''add_fractions_p''))) @@ |
186 [BOOL e_e, REAL v_v] |
186 (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e; |
187 in Check_elementwise L_L {(v_v::real). Assumptions})" |
187 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v] |
|
188 in |
|
189 Check_elementwise L_L {(v_v::real). Assumptions})" |
188 setup \<open>KEStore_Elems.add_mets |
190 setup \<open>KEStore_Elems.add_mets |
189 [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID |
191 [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID |
190 (["RatEq", "solve_rat_equation"], |
192 (["RatEq", "solve_rat_equation"], |
191 [("#Given" ,["equality e_e","solveFor v_v"]), |
193 [("#Given" ,["equality e_e","solveFor v_v"]), |
192 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
194 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |