36 |
36 |
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 (TermC.parse DiffApp.thy)) |
41 val c = (the o (TermC.parse Diff_App.thy)) |
42 "Program 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])\ |
56 |
56 |
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 (TermC.parse DiffApp.thy)) (*start interpretieren*) |
61 val sc = (the o (TermC.parse Diff_App.thy)) (*start interpretieren*) |
62 "Program 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_); \ |
72 \ [BOOL e_1, REAL v_1]);\ |
72 \ [BOOL e_1, REAL v_1]);\ |
73 \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
73 \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
74 \ [BOOL e_2, REAL v_2])\ |
74 \ [BOOL e_2, REAL v_2])\ |
75 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
75 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
76 |
76 |
77 val ags = map (Thm.term_of o the o (TermC.parse DiffApp.thy)) |
77 val ags = map (Thm.term_of o the o (TermC.parse Diff_App.thy)) |
78 ["A::real", "alpha::real", |
78 ["A::real", "alpha::real", |
79 "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"]; |
79 "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"]; |
80 val ll = [](*:loc_*); |
80 val ll = [](*:loc_*); |
81 (* problem with exn PTREE + eval_to ------------------------- |
81 (* problem with exn PTREE + eval_to ------------------------- |
82 "-------------- subproblem with empty formalizaton -------"; |
82 "-------------- subproblem with empty formalizaton -------"; |
90 (Substitute [("a", "#2*r*sin alpha"),("b", "#2*r*cos alpha")])); |
90 (Substitute [("a", "#2*r*sin alpha"),("b", "#2*r*cos alpha")])); |
91 "------- same_tacpbl + eval_to -------"; |
91 "------- same_tacpbl + eval_to -------"; |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
93 loc_2str l1; |
93 loc_2str l1; |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
95 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1; |
95 Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t1; |
96 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) |
96 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) |
97 |
97 |
98 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2); |
98 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2); |
99 loc_2str l2; |
99 loc_2str l2; |
100 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
100 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
101 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t2; |
101 Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t2; |
102 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) |
102 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) |
103 |
103 |
104 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3); |
104 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3); |
105 loc_2str l3; |
105 loc_2str l3; |
106 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) |
106 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) |
107 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t3; |
107 Syntax.string_of_term (ThyC.id_to_ctxt "Diff_App") t3; |
108 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) |
108 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) |
109 |
109 |
110 |
110 |
111 "------- eq_tacIDs + eq_consts + eval_args -------"; |
111 "------- eq_tacIDs + eq_consts + eval_args -------"; |
112 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; |
112 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; |