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 : set (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 ("Orderings.ord_class.less",eval_equ "#less_"),
69 Calc ("Orderings.ord_class.less_eq",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'*)
89 (prep_pbt thy "pbl_fun_max" [] e_pblID
90 (["maximum_of","function"],
91 [("#Given" ,["fixedValues f_ix"]),
92 ("#Find" ,["maximum m_m","valuesFor v_s"]),
93 ("#Relate",["relations r_s"])
98 (prep_pbt thy "pbl_fun_make" [] e_pblID
99 (["make","function"]:pblID,
100 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
101 ("#Find" ,["functionEq f_1"])
105 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
106 (["by_explicit","make","function"]:pblID,
107 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
108 ("#Find" ,["functionEq f_1"])
110 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
112 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
113 (["by_new_variable","make","function"]:pblID,
114 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
115 (*WN.12.5.03: precond for distinction still missing*)
116 ("#Find" ,["functionEq f_1"])
118 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
121 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
122 (["on_interval","maximum_of","function"]:pblID,
123 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
124 (*WN.12.5.03: precond for distinction still missing*)
125 ("#Find" ,["maxArgument v_0"])
130 (prep_pbt thy "pbl_tool" [] e_pblID
136 (prep_pbt thy "pbl_tool_findvals" [] e_pblID
137 (["find_values","tool"]:pblID,
138 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
139 ("#Find" ,["valuesFor v_ls"]),
140 ("#Relate",["additionalRels r_s"])
147 (** methods, scripts not yet implemented **)
150 (prep_met thy "met_diffapp" [] e_metID
153 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
154 crls = Atools_erls, nrls=norm_Rational
155 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
159 (prep_met thy "met_diffapp_max" [] e_metID
160 (["DiffApp","max_by_calculus"]:metID,
161 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s",
162 "boundVariable v_v","interval i_tv","errorBound e_rr"]),
163 ("#Find" ,["valuesFor v_s"]),
166 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
167 crls = eval_rls, nrls=norm_Rational
168 (*, asm_rls=[],asm_thm=[]*)},
169 "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
170 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
171 " (let e_e = (hd o (filterVar m_m)) r_s; " ^
172 " t_t = (if 1 < LENGTH r_s " ^
173 " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
174 " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
175 " else (hd r_s)); " ^
177 "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
178 " [DiffApp,max_on_interval_by_calculus]) " ^
179 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
180 " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
181 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
182 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "
187 (prep_met thy "met_diffapp_funnew" [] e_metID
188 (["DiffApp","make_fun_by_new_variable"]:metID,
189 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
190 ("#Find" ,["functionEq f_1"])
192 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
193 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
194 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
195 " (eqs::bool list) = " ^
196 "(let h_h = (hd o (filterVar f_f)) eqs; " ^
197 " e_s = dropWhile (ident h_h) eqs; " ^
198 " v_s = dropWhile (ident f_f) (Vars h_h); " ^
199 " v_1 = NTH 1 v_s; " ^
200 " v_2 = NTH 2 v_s; " ^
201 " e_1 = (hd o (filterVar v_1)) e_s; " ^
202 " e_2 = (hd o (filterVar v_2)) e_s; " ^
203 " (s_1::bool list) = " ^
204 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
205 " [BOOL e_1, REAL v_1]); " ^
206 " (s_2::bool list) = " ^
207 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
208 " [BOOL e_2, REAL v_2])" ^
209 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"
214 (prep_met thy "met_diffapp_funexp" [] e_metID
215 (["DiffApp","make_fun_by_explicit"]:metID,
216 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
217 ("#Find" ,["functionEq f_1"])
219 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
220 crls = eval_rls, nrls=norm_Rational
221 (*, asm_rls=[],asm_thm=[]*)},
222 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
223 " (eqs::bool list) = " ^
224 " (let h_h = (hd o (filterVar f_f)) eqs; " ^
225 " e_1 = hd (dropWhile (ident h_h) eqs); " ^
226 " v_s = dropWhile (ident f_f) (Vars h_h); " ^
227 " v_1 = hd (dropWhile (ident v_v) v_s); " ^
228 " (s_1::bool list)= " ^
229 " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
230 " [BOOL e_1, REAL v_1]) " ^
231 " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
236 (prep_met thy "met_diffapp_max_oninterval" [] e_metID
237 (["DiffApp","max_on_interval_by_calculus"]:metID,
238 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*,
239 "errorBound e_rr"*)]),
240 ("#Find" ,["maxArgument v_0"])
242 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
243 crls = eval_rls, nrls=norm_Rational
244 (*, asm_rls=[],asm_thm=[]*)},
250 (prep_met thy "met_diffapp_findvals" [] e_metID
251 (["DiffApp","find_values"]:metID,
253 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
254 crls = eval_rls, nrls=norm_Rational(*,
255 asm_rls=[],asm_thm=[]*)},
258 val list_rls = append_rls "list_rls" list_rls
259 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
260 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})
262 ruleset' := overwritelthy @{theory} (!ruleset',
263 [("list_rls",list_rls)