37 " ################################################# 6.5.03"; |
37 " ################################################# 6.5.03"; |
38 " scripts: Variante 'funktional' 6.5.03"; |
38 " scripts: Variante 'funktional' 6.5.03"; |
39 " ################################################# 6.5.03 "; |
39 " ################################################# 6.5.03 "; |
40 |
40 |
41 val c = (the o (parse DiffApp.thy)) |
41 val c = (the o (parse DiffApp.thy)) |
42 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ |
42 "Program Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ |
43 \ (v_::real) (itv_::real set) (err_::bool) = \ |
43 \ (v_::real) (itv_::real set) (err_::bool) = \ |
44 \ (let e_e = (hd o (filterVar m_)) rs_; \ |
44 \ (let e_e = (hd o (filterVar m_)) rs_; \ |
45 \ t_ = (if 1 < length_ rs_ \ |
45 \ t_ = (if 1 < length_ rs_ \ |
46 \ then (SubProblem (Reals_s,[make,function],[no_met])\ |
46 \ then (SubProblem (Reals_s,[make,function],[no_met])\ |
47 \ [REAL m_, REAL v_v, BOOL_LIST rs_])\ |
47 \ [REAL m_, REAL v_v, BOOL_LIST rs_])\ |
57 "################################################### 6.5.03"; |
57 "################################################### 6.5.03"; |
58 "############## Make_fun_by_new_variable ########### 6.5.03"; |
58 "############## Make_fun_by_new_variable ########### 6.5.03"; |
59 "################################################### 6.5.03"; |
59 "################################################### 6.5.03"; |
60 |
60 |
61 val sc = (the o (parse DiffApp.thy)) (*start interpretieren*) |
61 val sc = (the o (parse DiffApp.thy)) (*start interpretieren*) |
62 "Script Make_fun_by_new_variable (f_::real) (v_::real) \ |
62 "Program Make_fun_by_new_variable (f_::real) (v_::real) \ |
63 \ (eqs_::bool list) = \ |
63 \ (eqs_::bool list) = \ |
64 \(let h_ = (hd o (filterVar f_)) eqs_; \ |
64 \(let h_ = (hd o (filterVar f_)) eqs_; \ |
65 \ es_ = dropWhile (ident h_) eqs_; \ |
65 \ es_ = dropWhile (ident h_) eqs_; \ |
66 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
66 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
67 \ v_1 = nth_ 1 vs_; \ |
67 \ v_1 = nth_ 1 vs_; \ |
140 |
140 |
141 "############## Make_fun_by_explicit ############## 6.5.03"; |
141 "############## Make_fun_by_explicit ############## 6.5.03"; |
142 "############## Make_fun_by_explicit ############## 6.5.03"; |
142 "############## Make_fun_by_explicit ############## 6.5.03"; |
143 "############## Make_fun_by_explicit ############## 6.5.03"; |
143 "############## Make_fun_by_explicit ############## 6.5.03"; |
144 val c = (the o (parse DiffApp.thy)) |
144 val c = (the o (parse DiffApp.thy)) |
145 "Script Make_fun_by_explicit (f_::real) (v_::real) \ |
145 "Program Make_fun_by_explicit (f_::real) (v_::real) \ |
146 \ (eqs_::bool list) = \ |
146 \ (eqs_::bool list) = \ |
147 \ (let h_ = (hd o (filterVar f_)) eqs_; \ |
147 \ (let h_ = (hd o (filterVar f_)) eqs_; \ |
148 \ e_1 = hd (dropWhile (ident h_) eqs_); \ |
148 \ e_1 = hd (dropWhile (ident h_) eqs_); \ |
149 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
149 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
150 \ v_1 = hd (dropWhile (ident v_v) vs_); \ |
150 \ v_1 = hd (dropWhile (ident v_v) vs_); \ |
155 |
155 |
156 (*#####################################################--------11.5.02 |
156 (*#####################################################--------11.5.02 |
157 "################ Solve_root_equation #################"; |
157 "################ Solve_root_equation #################"; |
158 (*#####################################################*) |
158 (*#####################################################*) |
159 val sc = (Thm.term_of o the o (parse Test.thy)) |
159 val sc = (Thm.term_of o the o (parse Test.thy)) |
160 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ |
160 "Program Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ |
161 \ (let e_e = Rewrite square_equation_left True eq_; \ |
161 \ (let e_e = Rewrite square_equation_left True eq_; \ |
162 \ e_e = Rewrite_Set Test_simplify False e_; \ |
162 \ e_e = Rewrite_Set Test_simplify False e_; \ |
163 \ e_e = Rewrite_Set rearrange_assoc False e_; \ |
163 \ e_e = Rewrite_Set rearrange_assoc False e_; \ |
164 \ e_e = Rewrite_Set isolate_root False e_; \ |
164 \ e_e = Rewrite_Set isolate_root False e_; \ |
165 \ e_e = Rewrite_Set Test_simplify False e_; \ |
165 \ e_e = Rewrite_Set Test_simplify False e_; \ |
247 " --- test100: nxt_tac order------------------------------------ "; |
247 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
249 |
249 |
250 val scr as (Prog sc) = Prog (((inst_abs Test.thy) |
250 val scr as (Prog sc) = Prog (((inst_abs Test.thy) |
251 o Thm.term_of o the o (parse thy)) |
251 o Thm.term_of o the o (parse thy)) |
252 "Script Testeq (e_e::bool) = \ |
252 "Program Testeq (e_e::bool) = \ |
253 \(While (contains_root e_e) Do \ |
253 \(While (contains_root e_e) Do \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
256 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
256 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
257 \ e_e "); |
257 \ e_e "); |
268 val p = ([1],Res):pos'; |
268 val p = ([1],Res):pos'; |
269 val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; |
269 val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; |
270 |
270 |
271 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
271 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
272 val ve0_= (Thm.term_of o the o (parse thy)) ct; |
272 val ve0_= (Thm.term_of o the o (parse thy)) ct; |
273 val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
273 val ets0=[([],(Tac_(Program.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
274 e_term,e_term,Safe)), |
274 e_term,e_term,Safe)), |
275 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
275 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
276 val l0 = []; |
276 val l0 = []; |
277 " --------------- 1. ---------------------------------------------"; |
277 " --------------- 1. ---------------------------------------------"; |
278 val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete; |
278 val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete; |
281 *) |
281 *) |
282 |
282 |
283 |
283 |
284 val scr as (Prog sc) = |
284 val scr as (Prog sc) = |
285 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
285 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
286 "Script Testterm (g_::real) = (Calculate cancel g_)"); |
286 "Program Testterm (g_::real) = (Calculate cancel g_)"); |
287 (* |
287 (* |
288 val scr as (Prog sc) = |
288 val scr as (Prog sc) = |
289 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
289 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
290 "Script Testterm (g_::real) = (Calculate power g_)"); |
290 "Program Testterm (g_::real) = (Calculate power g_)"); |
291 val scr as (Prog sc) = |
291 val scr as (Prog sc) = |
292 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
292 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
293 "Script Testterm (g_::real) = (Calculate pow g_)"); |
293 "Program Testterm (g_::real) = (Calculate pow g_)"); |
294 ..............................................................*) |
294 ..............................................................*) |
295 writeln |
295 writeln |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |
298 \ (Repeat (Calculate power g_)) Or \n\ |
298 \ (Repeat (Calculate power g_)) Or \n\ |