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 "Script 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_,[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_])\ |
48 \ else (hd rs_)); \ |
48 \ else (hd rs_)); \ |
49 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \ |
49 \ (mx_::real) = SubProblem (Reals_s,[on_interval,max_of,function], \ |
50 \ [Isac,maximum_on_interval])\ |
50 \ [Isac,maximum_on_interval])\ |
51 \ [BOOL t_, REAL v_v, REAL_SET itv_]\ |
51 \ [BOOL t_, REAL v_v, REAL_SET itv_]\ |
52 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \ |
52 \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \ |
53 \ [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, \ |
53 \ [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, \ |
54 \ BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))"; |
54 \ BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))"; |
55 |
55 |
56 |
56 |
57 "################################################### 6.5.03"; |
57 "################################################### 6.5.03"; |
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_; \ |
68 \ v_2 = nth_ 2 vs_; \ |
68 \ v_2 = nth_ 2 vs_; \ |
69 \ e_1 = (hd o (filterVar v_1)) es_; \ |
69 \ e_1 = (hd o (filterVar v_1)) es_; \ |
70 \ e_2 = (hd o (filterVar v_2)) es_; \ |
70 \ e_2 = (hd o (filterVar v_2)) es_; \ |
71 \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
71 \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
72 \ [BOOL e_1, REAL v_1]);\ |
72 \ [BOOL e_1, REAL v_1]);\ |
73 \ (s_2::bool list) = (SubProblem (Reals_,[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 (parse DiffApp.thy)) |
77 val ags = map (Thm.term_of o the o (parse DiffApp.thy)) |
78 ["A::real", "alpha::real", |
78 ["A::real", "alpha::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_); \ |
151 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\ |
151 \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\ |
152 \ [BOOL e_1, REAL v_1])\ |
152 \ [BOOL e_1, REAL v_1])\ |
153 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; |
153 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; |
154 |
154 |
155 |
155 |
156 (*#####################################################--------11.5.02 |
156 (*#####################################################--------11.5.02 |