94 e_rls, NONE, [])); |
94 e_rls, NONE, [])); |
95 |
95 |
96 store_pbt |
96 store_pbt |
97 (prep_pbt thy "pbl_fun_make" [] e_pblID |
97 (prep_pbt thy "pbl_fun_make" [] e_pblID |
98 (["make","function"]:pblID, |
98 (["make","function"]:pblID, |
99 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), |
99 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
100 ("#Find" ,["functionEq f_1_"]) |
100 ("#Find" ,["functionEq f_1_"]) |
101 ], |
101 ], |
102 e_rls, NONE, [])); |
102 e_rls, NONE, [])); |
103 store_pbt |
103 store_pbt |
104 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID |
104 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID |
105 (["by_explicit","make","function"]:pblID, |
105 (["by_explicit","make","function"]:pblID, |
106 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), |
106 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
107 ("#Find" ,["functionEq f_1_"]) |
107 ("#Find" ,["functionEq f_1_"]) |
108 ], |
108 ], |
109 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); |
109 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); |
110 store_pbt |
110 store_pbt |
111 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID |
111 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID |
112 (["by_new_variable","make","function"]:pblID, |
112 (["by_new_variable","make","function"]:pblID, |
113 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), |
113 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
114 (*WN.12.5.03: precond for distinction still missing*) |
114 (*WN.12.5.03: precond for distinction still missing*) |
115 ("#Find" ,["functionEq f_1_"]) |
115 ("#Find" ,["functionEq f_1_"]) |
116 ], |
116 ], |
117 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])); |
117 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])); |
118 |
118 |
132 e_rls, NONE, [])); |
132 e_rls, NONE, [])); |
133 |
133 |
134 store_pbt |
134 store_pbt |
135 (prep_pbt thy "pbl_tool_findvals" [] e_pblID |
135 (prep_pbt thy "pbl_tool_findvals" [] e_pblID |
136 (["find_values","tool"]:pblID, |
136 (["find_values","tool"]:pblID, |
137 [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]), |
137 [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]), |
138 ("#Find" ,["valuesFor vls_"]), |
138 ("#Find" ,["valuesFor vls_"]), |
139 ("#Relate",["additionalRels rs_"]) |
139 ("#Relate",["additionalRels rs_"]) |
140 ], |
140 ], |
141 e_rls, NONE, [])); |
141 e_rls, NONE, [])); |
142 |
142 |
177 " BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) " |
177 " BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) " |
178 )); |
178 )); |
179 store_met |
179 store_met |
180 (prep_met thy "met_diffapp_funnew" [] e_metID |
180 (prep_met thy "met_diffapp_funnew" [] e_metID |
181 (["DiffApp","make_fun_by_new_variable"]:metID, |
181 (["DiffApp","make_fun_by_new_variable"]:metID, |
182 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), |
182 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
183 ("#Find" ,["functionEq f_1_"]) |
183 ("#Find" ,["functionEq f_1_"]) |
184 ], |
184 ], |
185 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, |
185 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, |
186 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
186 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
187 "Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^ |
187 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ |
188 " (eqs_::bool list) = " ^ |
188 " (eqs::bool list) = " ^ |
189 "(let h_ = (hd o (filterVar f_)) eqs_; " ^ |
189 "(let h_ = (hd o (filterVar f_)) eqs; " ^ |
190 " es_ = dropWhile (ident h_) eqs_; " ^ |
190 " es_ = dropWhile (ident h_) eqs; " ^ |
191 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
191 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
192 " v_1 = nth_ 1 vs_; " ^ |
192 " v_1 = nth_ 1 vs_; " ^ |
193 " v_2 = nth_ 2 vs_; " ^ |
193 " v_2 = nth_ 2 vs_; " ^ |
194 " e_1 = (hd o (filterVar v_1)) es_; " ^ |
194 " e_1 = (hd o (filterVar v_1)) es_; " ^ |
195 " e_2 = (hd o (filterVar v_2)) es_; " ^ |
195 " e_2 = (hd o (filterVar v_2)) es_; " ^ |
202 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)" |
202 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)" |
203 )); |
203 )); |
204 store_met |
204 store_met |
205 (prep_met thy "met_diffapp_funexp" [] e_metID |
205 (prep_met thy "met_diffapp_funexp" [] e_metID |
206 (["DiffApp","make_fun_by_explicit"]:metID, |
206 (["DiffApp","make_fun_by_explicit"]:metID, |
207 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), |
207 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
208 ("#Find" ,["functionEq f_1_"]) |
208 ("#Find" ,["functionEq f_1_"]) |
209 ], |
209 ], |
210 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
210 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
211 crls = eval_rls, nrls=norm_Rational |
211 crls = eval_rls, nrls=norm_Rational |
212 (*, asm_rls=[],asm_thm=[]*)}, |
212 (*, asm_rls=[],asm_thm=[]*)}, |
213 "Script Make_fun_by_explicit (f_::real) (v_v::real) " ^ |
213 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ |
214 " (eqs_::bool list) = " ^ |
214 " (eqs::bool list) = " ^ |
215 " (let h_ = (hd o (filterVar f_)) eqs_; " ^ |
215 " (let h_ = (hd o (filterVar f_)) eqs; " ^ |
216 " e_1 = hd (dropWhile (ident h_) eqs_); " ^ |
216 " e_1 = hd (dropWhile (ident h_) eqs); " ^ |
217 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
217 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
218 " v_1 = hd (dropWhile (ident v_v) vs_); " ^ |
218 " v_1 = hd (dropWhile (ident v_v) vs_); " ^ |
219 " (s_1::bool list)= " ^ |
219 " (s_1::bool list)= " ^ |
220 " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^ |
220 " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^ |
221 " [BOOL e_1, REAL v_1]) " ^ |
221 " [BOOL e_1, REAL v_1]) " ^ |