135 |
135 |
136 store_pbt |
136 store_pbt |
137 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
137 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
138 (["rat","sq","root","univariate","equation"], |
138 (["rat","sq","root","univariate","equation"], |
139 [("#Given" ,["equality e_e","solveFor v_v"]), |
139 [("#Given" ,["equality e_e","solveFor v_v"]), |
140 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_::real) )| " ^ |
140 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ |
141 "( (rhs e_e) is_rootRatAddTerm_in (v_::real) )"]), |
141 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
142 ("#Find" ,["solutions v_i"]) |
142 ("#Find" ,["solutions v_i"]) |
143 ], |
143 ], |
144 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
144 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
145 [["RootRatEq","elim_rootrat_equation"]])); |
145 [["RootRatEq","elim_rootrat_equation"]])); |
146 |
146 |
154 (*-- left 20.10.02 --*) |
154 (*-- left 20.10.02 --*) |
155 store_met |
155 store_met |
156 (prep_met thy "met_rootrateq_elim" [] e_metID |
156 (prep_met thy "met_rootrateq_elim" [] e_metID |
157 (["RootRatEq","elim_rootrat_equation"], |
157 (["RootRatEq","elim_rootrat_equation"], |
158 [("#Given" ,["equality e_e","solveFor v_v"]), |
158 [("#Given" ,["equality e_e","solveFor v_v"]), |
159 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_::real) ) | " ^ |
159 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^ |
160 "( (rhs e_e) is_rootRatAddTerm_in (v_::real) )"]), |
160 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
161 ("#Find" ,["solutions v_i"]) |
161 ("#Find" ,["solutions v_i"]) |
162 ], |
162 ], |
163 {rew_ord'="termlessI", |
163 {rew_ord'="termlessI", |
164 rls'=RooRatEq_erls, |
164 rls'=RooRatEq_erls, |
165 srls=e_rls, |
165 srls=e_rls, |
166 prls=RootRatEq_prls, |
166 prls=RootRatEq_prls, |
167 calc=[], |
167 calc=[], |
168 crls=RootRatEq_crls, nrls=norm_Rational(*, |
168 crls=RootRatEq_crls, nrls=norm_Rational(*, |
169 asm_rls=[], |
169 asm_rls=[], |
170 asm_thm=[]*)}, |
170 asm_thm=[]*)}, |
171 "Script Elim_rootrat_equation (e_e::bool) (v_::real) = " ^ |
171 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^ |
172 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^ |
172 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^ |
173 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
173 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
174 " (Try (Rewrite_Set make_rooteq False)) @@ " ^ |
174 " (Try (Rewrite_Set make_rooteq False)) @@ " ^ |
175 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
175 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
176 " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^ |
176 " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^ |