1 (* application of differential calculus
3 (c) due to copyright terms
6 theory DiffApp imports Diff begin
11 :: "[bool list,real,bool list,real,real set,bool,
12 bool list] => bool list"
13 ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
15 Make'_fun'_by'_new'_variable
16 :: "[real,real,bool list,
18 ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))//
20 Make'_fun'_by'_explicit
21 :: "[real,real,bool list,
23 ("((Script Make'_fun'_by'_explicit (_ _ _ =))//
28 (*for script Maximum_value*)
29 filterVar :: "[real, 'a list] => 'a list"
32 filterVar_Nil "filterVar v [] = []"
33 filterVar_Const "filterVar v (x#xs) =
34 (if (v mem (Vars x)) then x#(filterVar v xs)
35 else filterVar v xs) "
36 text {*WN.6.5.03: old decisions in this file partially are being changed
37 in a quick-and-dirty way to make scripts run: Maximum_value,
38 Make_fun_by_new_variable, Make_fun_by_explicit.
39 found to be reconsidered:
40 - descriptions (Descript.thy)
41 - penv: really need term list; or just rerun the whole example with num/var
42 - mk_arg, itms2args ... env in script different from penv ?
43 - L = SubProblem eq ... show some vars on the worksheet ? (other means for
44 referencing are labels (no on worksheet))
46 WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env
51 val eval_rls = prep_rls(
52 Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
53 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
54 rules = [Thm ("refl",num_str @{refl),
55 Thm ("real_le_refl",num_str @{thm real_le_refl}),
56 Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
57 Thm ("not_true",num_str @{not_true),
58 Thm ("not_false",num_str @{not_false),
59 Thm ("and_true",and_true),
60 Thm ("and_false",and_false),
61 Thm ("or_true",or_true),
62 Thm ("or_false",or_false),
63 Thm ("and_commute",num_str @{and_commute),
64 Thm ("or_commute",num_str @{or_commute),
66 Calc ("op <",eval_equ "#less_"),
67 Calc ("op <=",eval_equ "#less_equal_"),
69 Calc ("Atools.ident",eval_ident "#ident_"),
70 Calc ("Atools.is'_const",eval_const "#is_const_"),
71 Calc ("Atools.occurs'_in",eval_occurs_in ""),
72 Calc ("Tools.matches",eval_matches "")
74 scr = Script ((term_of o the o (parse thy))
77 ruleset' := overwritelthy thy
79 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
86 (prep_pbt (theory "DiffApp") "pbl_fun_max" [] e_pblID
87 (["maximum_of","function"],
88 [("#Given" ,["fixedValues fix_"]),
89 ("#Find" ,["maximum m_","valuesFor vs_"]),
90 ("#Relate",["relations rs_"])
95 (prep_pbt (theory "DiffApp") "pbl_fun_make" [] e_pblID
96 (["make","function"]:pblID,
97 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
98 ("#Find" ,["functionEq f_1_"])
102 (prep_pbt (theory "DiffApp") "pbl_fun_max_expl" [] e_pblID
103 (["by_explicit","make","function"]:pblID,
104 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
105 ("#Find" ,["functionEq f_1_"])
107 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
109 (prep_pbt (theory "DiffApp") "pbl_fun_max_newvar" [] e_pblID
110 (["by_new_variable","make","function"]:pblID,
111 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
112 (*WN.12.5.03: precond for distinction still missing*)
113 ("#Find" ,["functionEq f_1_"])
115 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
118 (prep_pbt (theory "DiffApp") "pbl_fun_max_interv" [] e_pblID
119 (["on_interval","maximum_of","function"]:pblID,
120 [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"]),
121 (*WN.12.5.03: precond for distinction still missing*)
122 ("#Find" ,["maxArgument v_0_"])
127 (prep_pbt (theory "DiffApp") "pbl_tool" [] e_pblID
133 (prep_pbt (theory "DiffApp") "pbl_tool_findvals" [] e_pblID
134 (["find_values","tool"]:pblID,
135 [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_"]),
136 ("#Find" ,["valuesFor vls_"]),
137 ("#Relate",["additionalRels rs_"])
142 (** methods, scripts not yet implemented **)
145 (prep_met (theory "DiffApp") "met_diffapp" [] e_metID
148 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
149 crls = Atools_erls, nrls=norm_Rational
150 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
152 (prep_met (theory "DiffApp") "met_diffapp_max" [] e_metID
153 (["DiffApp","max_by_calculus"]:metID,
154 [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
155 "boundVariable v_","interval itv_","errorBound err_"]),
156 ("#Find" ,["valuesFor vs_"]),
159 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
160 crls = eval_rls, nrls=norm_Rational
161 (*, asm_rls=[],asm_thm=[]*)},
162 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^
163 " (v_::real) (itv_::real set) (err_::bool) = " ^
164 " (let e_ = (hd o (filterVar m_)) rs_; " ^
165 " t_ = (if 1 < length_ rs_ " ^
166 " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^
167 " [real_ m_, real_ v_, bool_list_ rs_]) " ^
168 " else (hd rs_)); " ^
170 "SubProblem(DiffApp_,[on_interval,maximum_of,function], " ^
171 " [DiffApp,max_on_interval_by_calculus]) " ^
172 " [bool_ t_, real_ v_, real_set_ itv_] " ^
173 " in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) " ^
174 " [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, " ^
175 " bool_list_ (dropWhile (ident e_) rs_)])::bool list)) "
178 (prep_met (theory "DiffApp") "met_diffapp_funnew" [] e_metID
179 (["DiffApp","make_fun_by_new_variable"]:metID,
180 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
181 ("#Find" ,["functionEq f_1_"])
183 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
184 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
185 "Script Make_fun_by_new_variable (f_::real) (v_::real) " ^
186 " (eqs_::bool list) = " ^
187 "(let h_ = (hd o (filterVar f_)) eqs_; " ^
188 " es_ = dropWhile (ident h_) eqs_; " ^
189 " vs_ = dropWhile (ident f_) (Vars h_); " ^
190 " v_1 = nth_ 1 vs_; " ^
191 " v_2 = nth_ 2 vs_; " ^
192 " e_1 = (hd o (filterVar v_1)) es_; " ^
193 " e_2 = (hd o (filterVar v_2)) es_; " ^
194 " (s_1::bool list) = " ^
195 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
196 " [bool_ e_1, real_ v_1]); " ^
197 " (s_2::bool list) = " ^
198 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
199 " [bool_ e_2, real_ v_2])" ^
200 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
203 (prep_met (theory "DiffApp") "met_diffapp_funexp" [] e_metID
204 (["DiffApp","make_fun_by_explicit"]:metID,
205 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
206 ("#Find" ,["functionEq f_1_"])
208 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
209 crls = eval_rls, nrls=norm_Rational
210 (*, asm_rls=[],asm_thm=[]*)},
211 "Script Make_fun_by_explicit (f_::real) (v_::real) " ^
212 " (eqs_::bool list) = " ^
213 " (let h_ = (hd o (filterVar f_)) eqs_; " ^
214 " e_1 = hd (dropWhile (ident h_) eqs_); " ^
215 " vs_ = dropWhile (ident f_) (Vars h_); " ^
216 " v_1 = hd (dropWhile (ident v_) vs_); " ^
217 " (s_1::bool list)= " ^
218 " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^
219 " [bool_ e_1, real_ v_1]) " ^
220 " in Substitute [(v_1 = (rhs o hd) s_1)] h_) "
223 (prep_met (theory "DiffApp") "met_diffapp_max_oninterval" [] e_metID
224 (["DiffApp","max_on_interval_by_calculus"]:metID,
225 [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"(*,
226 "errorBound err_"*)]),
227 ("#Find" ,["maxArgument v_0_"])
229 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
230 crls = eval_rls, nrls=norm_Rational
231 (*, asm_rls=[],asm_thm=[]*)},
235 (prep_met (theory "DiffApp") "met_diffapp_findvals" [] e_metID
236 (["DiffApp","find_values"]:metID,
238 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
239 crls = eval_rls, nrls=norm_Rational(*,
240 asm_rls=[],asm_thm=[]*)},
243 val list_rls = append_rls "list_rls" list_rls
244 [Thm ("filterVar_Const", num_str @{filterVar_Const),
245 Thm ("filterVar_Nil", num_str @{filterVar_Nil)
247 ruleset' := overwritelthy thy (!ruleset',
248 [("list_rls",list_rls)