138 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
138 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
139 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
139 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
140 "empty_script")] |
140 "empty_script")] |
141 \<close> |
141 \<close> |
142 (* ansprechen mit ["LinEq","solve_univar_equation"] *) |
142 (* ansprechen mit ["LinEq","solve_univar_equation"] *) |
|
143 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
|
144 where |
|
145 "solve_linear_equation e_e v_v = |
|
146 (let e_e =((Try (Rewrite ''all_left'' False)) @@ |
|
147 (Try (Repeat (Rewrite ''makex1_x'' False))) @@ |
|
148 (Try (Rewrite_Set ''expand_binoms'' False)) @@ |
|
149 (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] |
|
150 ''make_ratpoly_in'' False))) @@ |
|
151 (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e; |
|
152 e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)] |
|
153 ''LinEq_simplify'' True)) @@ |
|
154 (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e |
|
155 in Or_to_List e_e)" |
143 setup \<open>KEStore_Elems.add_mets |
156 setup \<open>KEStore_Elems.add_mets |
144 [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID |
157 [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID |
145 (["LinEq","solve_lineq_equation"], |
158 (["LinEq","solve_lineq_equation"], |
146 [("#Given", ["equality e_e", "solveFor v_v"]), |
159 [("#Given", ["equality e_e", "solveFor v_v"]), |
147 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), |
160 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), |