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
53 val eval_rls = prep_rls(
54 Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
55 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
56 rules = [Thm ("refl",num_str @{thm refl}),
57 Thm ("real_le_refl",num_str @{thm real_le_refl}),
58 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
59 Thm ("not_true",num_str @{thm not_true}),
60 Thm ("not_false",num_str @{thm not_false}),
61 Thm ("and_true",num_str @{thm and_true}),
62 Thm ("and_false",num_str @{thm and_false}),
63 Thm ("or_true",num_str @{thm or_true}),
64 Thm ("or_false",num_str @{thm or_false}),
65 Thm ("and_commute",num_str @{thm and_commute}),
66 Thm ("or_commute",num_str @{thm or_commute}),
68 Calc ("op <",eval_equ "#less_"),
69 Calc ("op <=",eval_equ "#less_equal_"),
71 Calc ("Atools.ident",eval_ident "#ident_"),
72 Calc ("Atools.is'_const",eval_const "#is_const_"),
73 Calc ("Atools.occurs'_in",eval_occurs_in ""),
74 Calc ("Tools.matches",eval_matches "")
76 scr = Script ((term_of o the o (parse thy))
79 ruleset' := overwritelthy @{theory}
81 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
88 (prep_pbt thy "pbl_fun_max" [] e_pblID
89 (["maximum_of","function"],
90 [("#Given" ,["fixedValues fix_"]),
91 ("#Find" ,["maximum m_","valuesFor vs_"]),
92 ("#Relate",["relations rs_"])
97 (prep_pbt thy "pbl_fun_make" [] e_pblID
98 (["make","function"]:pblID,
99 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
100 ("#Find" ,["functionEq f_1_"])
104 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
105 (["by_explicit","make","function"]:pblID,
106 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
107 ("#Find" ,["functionEq f_1_"])
109 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
111 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
112 (["by_new_variable","make","function"]:pblID,
113 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
114 (*WN.12.5.03: precond for distinction still missing*)
115 ("#Find" ,["functionEq f_1_"])
117 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
120 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
121 (["on_interval","maximum_of","function"]:pblID,
122 [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"]),
123 (*WN.12.5.03: precond for distinction still missing*)
124 ("#Find" ,["maxArgument v_0_"])
129 (prep_pbt thy "pbl_tool" [] e_pblID
135 (prep_pbt thy "pbl_tool_findvals" [] e_pblID
136 (["find_values","tool"]:pblID,
137 [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]),
138 ("#Find" ,["valuesFor vls_"]),
139 ("#Relate",["additionalRels rs_"])
144 (** methods, scripts not yet implemented **)
147 (prep_met thy "met_diffapp" [] e_metID
150 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
151 crls = Atools_erls, nrls=norm_Rational
152 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
154 (prep_met thy "met_diffapp_max" [] e_metID
155 (["DiffApp","max_by_calculus"]:metID,
156 [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
157 "boundVariable v_v","interval itv_","errorBound err_"]),
158 ("#Find" ,["valuesFor vs_"]),
161 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
162 crls = eval_rls, nrls=norm_Rational
163 (*, asm_rls=[],asm_thm=[]*)},
164 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^
165 " (v_v::real) (itv_v::real set) (err_::bool) = " ^
166 " (let e_e = (hd o (filterVar m_)) rs_; " ^
167 " t_ = (if 1 < length_ rs_ " ^
168 " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^
169 " [REAL m_, REAL v_v, BOOL_LIST rs_]) " ^
170 " else (hd rs_)); " ^
172 "SubProblem(DiffApp_,[on_interval,maximum_of,function], " ^
173 " [DiffApp,max_on_interval_by_calculus]) " ^
174 " [BOOL t_, REAL v_v, REAL_SET itv_] " ^
175 " in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) " ^
176 " [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, " ^
177 " BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) "
180 (prep_met thy "met_diffapp_funnew" [] e_metID
181 (["DiffApp","make_fun_by_new_variable"]:metID,
182 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
183 ("#Find" ,["functionEq f_1_"])
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=[]*)},
187 "Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^
188 " (eqs_::bool list) = " ^
189 "(let h_ = (hd o (filterVar f_)) eqs_; " ^
190 " es_ = dropWhile (ident h_) eqs_; " ^
191 " vs_ = dropWhile (ident f_) (Vars h_); " ^
192 " v_1 = nth_ 1 vs_; " ^
193 " v_2 = nth_ 2 vs_; " ^
194 " e_1 = (hd o (filterVar v_1)) es_; " ^
195 " e_2 = (hd o (filterVar v_2)) es_; " ^
196 " (s_1::bool list) = " ^
197 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
198 " [BOOL e_1, REAL v_1]); " ^
199 " (s_2::bool list) = " ^
200 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
201 " [BOOL e_2, REAL v_2])" ^
202 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
205 (prep_met thy "met_diffapp_funexp" [] e_metID
206 (["DiffApp","make_fun_by_explicit"]:metID,
207 [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
208 ("#Find" ,["functionEq f_1_"])
210 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
211 crls = eval_rls, nrls=norm_Rational
212 (*, asm_rls=[],asm_thm=[]*)},
213 "Script Make_fun_by_explicit (f_::real) (v_v::real) " ^
214 " (eqs_::bool list) = " ^
215 " (let h_ = (hd o (filterVar f_)) eqs_; " ^
216 " e_1 = hd (dropWhile (ident h_) eqs_); " ^
217 " vs_ = dropWhile (ident f_) (Vars h_); " ^
218 " v_1 = hd (dropWhile (ident v_v) vs_); " ^
219 " (s_1::bool list)= " ^
220 " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^
221 " [BOOL e_1, REAL v_1]) " ^
222 " in Substitute [(v_1 = (rhs o hd) s_1)] h_) "
225 (prep_met thy "met_diffapp_max_oninterval" [] e_metID
226 (["DiffApp","max_on_interval_by_calculus"]:metID,
227 [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"(*,
228 "errorBound err_"*)]),
229 ("#Find" ,["maxArgument v_0_"])
231 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
232 crls = eval_rls, nrls=norm_Rational
233 (*, asm_rls=[],asm_thm=[]*)},
237 (prep_met thy "met_diffapp_findvals" [] e_metID
238 (["DiffApp","find_values"]:metID,
240 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
241 crls = eval_rls, nrls=norm_Rational(*,
242 asm_rls=[],asm_thm=[]*)},
245 val list_rls = append_rls "list_rls" list_rls
246 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
247 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})
249 ruleset' := overwritelthy @{theory} (!ruleset',
250 [("list_rls",list_rls)