neuper@37906
|
1 |
(* application of differential calculus
|
neuper@37954
|
2 |
Walther Neuper 2002
|
neuper@37954
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
neuper@37954
|
6 |
theory DiffApp imports Diff begin
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
consts
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
Maximum'_value
|
neuper@37954
|
11 |
:: "[bool list,real,bool list,real,real set,bool,
|
neuper@37954
|
12 |
bool list] => bool list"
|
neuper@37906
|
13 |
("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
Make'_fun'_by'_new'_variable
|
neuper@37954
|
16 |
:: "[real,real,bool list,
|
neuper@37954
|
17 |
bool] => bool"
|
neuper@37954
|
18 |
("((Script Make'_fun'_by'_new'_variable (_ _ _ =))//
|
neuper@37954
|
19 |
(_))" 9)
|
neuper@37906
|
20 |
Make'_fun'_by'_explicit
|
neuper@37954
|
21 |
:: "[real,real,bool list,
|
neuper@37954
|
22 |
bool] => bool"
|
neuper@37954
|
23 |
("((Script Make'_fun'_by'_explicit (_ _ _ =))//
|
neuper@37954
|
24 |
(_))" 9)
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
dummy :: real
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*for script Maximum_value*)
|
neuper@37906
|
29 |
filterVar :: "[real, 'a list] => 'a list"
|
neuper@37906
|
30 |
|
neuper@37983
|
31 |
(*primrec*)axioms
|
neuper@37906
|
32 |
filterVar_Nil "filterVar v [] = []"
|
neuper@37954
|
33 |
filterVar_Const "filterVar v (x#xs) =
|
neuper@37954
|
34 |
(if (v mem (Vars x)) then x#(filterVar v xs)
|
neuper@37954
|
35 |
else filterVar v xs) "
|
neuper@37954
|
36 |
text {*WN.6.5.03: old decisions in this file partially are being changed
|
neuper@37954
|
37 |
in a quick-and-dirty way to make scripts run: Maximum_value,
|
neuper@37954
|
38 |
Make_fun_by_new_variable, Make_fun_by_explicit.
|
neuper@37954
|
39 |
found to be reconsidered:
|
neuper@37954
|
40 |
- descriptions (Descript.thy)
|
neuper@37954
|
41 |
- penv: really need term list; or just rerun the whole example with num/var
|
neuper@37954
|
42 |
- mk_arg, itms2args ... env in script different from penv ?
|
neuper@37954
|
43 |
- L = SubProblem eq ... show some vars on the worksheet ? (other means for
|
neuper@37954
|
44 |
referencing are labels (no on worksheet))
|
neuper@37954
|
45 |
|
neuper@37954
|
46 |
WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env
|
neuper@37954
|
47 |
from penv as is.
|
neuper@37954
|
48 |
*}
|
neuper@37954
|
49 |
|
neuper@37954
|
50 |
ML {*
|
neuper@37972
|
51 |
val thy = @{theory};
|
neuper@37972
|
52 |
|
neuper@37954
|
53 |
val eval_rls = prep_rls(
|
neuper@37954
|
54 |
Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
|
neuper@37954
|
55 |
erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
|
neuper@37969
|
56 |
rules = [Thm ("refl",num_str @{thm refl}),
|
neuper@37965
|
57 |
Thm ("real_le_refl",num_str @{thm real_le_refl}),
|
neuper@37969
|
58 |
Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
|
neuper@37969
|
59 |
Thm ("not_true",num_str @{thm not_true}),
|
neuper@37969
|
60 |
Thm ("not_false",num_str @{thm not_false}),
|
neuper@37969
|
61 |
Thm ("and_true",num_str @{thm and_true}),
|
neuper@37969
|
62 |
Thm ("and_false",num_str @{thm and_false}),
|
neuper@37969
|
63 |
Thm ("or_true",num_str @{thm or_true}),
|
neuper@37969
|
64 |
Thm ("or_false",num_str @{thm or_false}),
|
neuper@37969
|
65 |
Thm ("and_commute",num_str @{thm and_commute}),
|
neuper@37969
|
66 |
Thm ("or_commute",num_str @{thm or_commute}),
|
neuper@37954
|
67 |
|
neuper@37954
|
68 |
Calc ("op <",eval_equ "#less_"),
|
neuper@37954
|
69 |
Calc ("op <=",eval_equ "#less_equal_"),
|
neuper@37954
|
70 |
|
neuper@37954
|
71 |
Calc ("Atools.ident",eval_ident "#ident_"),
|
neuper@37954
|
72 |
Calc ("Atools.is'_const",eval_const "#is_const_"),
|
neuper@37954
|
73 |
Calc ("Atools.occurs'_in",eval_occurs_in ""),
|
neuper@37954
|
74 |
Calc ("Tools.matches",eval_matches "")
|
neuper@37954
|
75 |
],
|
neuper@37954
|
76 |
scr = Script ((term_of o the o (parse thy))
|
neuper@37954
|
77 |
"empty_script")
|
neuper@37954
|
78 |
}:rls);
|
neuper@37967
|
79 |
ruleset' := overwritelthy @{theory}
|
neuper@37954
|
80 |
(!ruleset',
|
neuper@37954
|
81 |
[("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
|
neuper@37954
|
82 |
]);
|
neuper@37954
|
83 |
|
neuper@37954
|
84 |
|
neuper@37954
|
85 |
(** problem types **)
|
neuper@37954
|
86 |
|
neuper@37954
|
87 |
store_pbt
|
neuper@37972
|
88 |
(prep_pbt thy "pbl_fun_max" [] e_pblID
|
neuper@37954
|
89 |
(["maximum_of","function"],
|
neuper@37954
|
90 |
[("#Given" ,["fixedValues fix_"]),
|
neuper@37954
|
91 |
("#Find" ,["maximum m_","valuesFor vs_"]),
|
neuper@37954
|
92 |
("#Relate",["relations rs_"])
|
neuper@37954
|
93 |
],
|
neuper@37954
|
94 |
e_rls, NONE, []));
|
neuper@37954
|
95 |
|
neuper@37954
|
96 |
store_pbt
|
neuper@37972
|
97 |
(prep_pbt thy "pbl_fun_make" [] e_pblID
|
neuper@37954
|
98 |
(["make","function"]:pblID,
|
neuper@37981
|
99 |
[("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
|
neuper@37954
|
100 |
("#Find" ,["functionEq f_1_"])
|
neuper@37954
|
101 |
],
|
neuper@37954
|
102 |
e_rls, NONE, []));
|
neuper@37954
|
103 |
store_pbt
|
neuper@37972
|
104 |
(prep_pbt thy "pbl_fun_max_expl" [] e_pblID
|
neuper@37954
|
105 |
(["by_explicit","make","function"]:pblID,
|
neuper@37981
|
106 |
[("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
|
neuper@37954
|
107 |
("#Find" ,["functionEq f_1_"])
|
neuper@37954
|
108 |
],
|
neuper@37954
|
109 |
e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
|
neuper@37954
|
110 |
store_pbt
|
neuper@37972
|
111 |
(prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
|
neuper@37954
|
112 |
(["by_new_variable","make","function"]:pblID,
|
neuper@37981
|
113 |
[("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
|
neuper@37954
|
114 |
(*WN.12.5.03: precond for distinction still missing*)
|
neuper@37954
|
115 |
("#Find" ,["functionEq f_1_"])
|
neuper@37954
|
116 |
],
|
neuper@37954
|
117 |
e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
|
neuper@37954
|
118 |
|
neuper@37954
|
119 |
store_pbt
|
neuper@37972
|
120 |
(prep_pbt thy "pbl_fun_max_interv" [] e_pblID
|
neuper@37954
|
121 |
(["on_interval","maximum_of","function"]:pblID,
|
neuper@37981
|
122 |
[("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"]),
|
neuper@37954
|
123 |
(*WN.12.5.03: precond for distinction still missing*)
|
neuper@37954
|
124 |
("#Find" ,["maxArgument v_0_"])
|
neuper@37954
|
125 |
],
|
neuper@37954
|
126 |
e_rls, NONE, []));
|
neuper@37954
|
127 |
|
neuper@37954
|
128 |
store_pbt
|
neuper@37972
|
129 |
(prep_pbt thy "pbl_tool" [] e_pblID
|
neuper@37954
|
130 |
(["tool"]:pblID,
|
neuper@37954
|
131 |
[],
|
neuper@37954
|
132 |
e_rls, NONE, []));
|
neuper@37954
|
133 |
|
neuper@37954
|
134 |
store_pbt
|
neuper@37972
|
135 |
(prep_pbt thy "pbl_tool_findvals" [] e_pblID
|
neuper@37954
|
136 |
(["find_values","tool"]:pblID,
|
neuper@37981
|
137 |
[("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]),
|
neuper@37954
|
138 |
("#Find" ,["valuesFor vls_"]),
|
neuper@37954
|
139 |
("#Relate",["additionalRels rs_"])
|
neuper@37954
|
140 |
],
|
neuper@37954
|
141 |
e_rls, NONE, []));
|
neuper@37954
|
142 |
|
neuper@37954
|
143 |
|
neuper@37954
|
144 |
(** methods, scripts not yet implemented **)
|
neuper@37954
|
145 |
|
neuper@37954
|
146 |
store_met
|
neuper@37972
|
147 |
(prep_met thy "met_diffapp" [] e_metID
|
neuper@37954
|
148 |
(["DiffApp"],
|
neuper@37954
|
149 |
[],
|
neuper@37954
|
150 |
{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
|
neuper@37954
|
151 |
crls = Atools_erls, nrls=norm_Rational
|
neuper@37954
|
152 |
(*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
|
neuper@37954
|
153 |
store_met
|
neuper@37972
|
154 |
(prep_met thy "met_diffapp_max" [] e_metID
|
neuper@37954
|
155 |
(["DiffApp","max_by_calculus"]:metID,
|
neuper@37954
|
156 |
[("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
|
neuper@37981
|
157 |
"boundVariable v_v","interval itv_","errorBound err_"]),
|
neuper@37954
|
158 |
("#Find" ,["valuesFor vs_"]),
|
neuper@37954
|
159 |
("#Relate",[])
|
neuper@37954
|
160 |
],
|
neuper@37954
|
161 |
{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
|
neuper@37954
|
162 |
crls = eval_rls, nrls=norm_Rational
|
neuper@37954
|
163 |
(*, asm_rls=[],asm_thm=[]*)},
|
neuper@37954
|
164 |
"Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^
|
neuper@37991
|
165 |
" (v_v::real) (itv_v::real set) (err_::bool) = " ^
|
neuper@37981
|
166 |
" (let e_e = (hd o (filterVar m_)) rs_; " ^
|
neuper@37954
|
167 |
" t_ = (if 1 < length_ rs_ " ^
|
neuper@37954
|
168 |
" then (SubProblem (DiffApp_,[make,function],[no_met]) " ^
|
neuper@37984
|
169 |
" [REAL m_, REAL v_v, BOOL_LIST rs_]) " ^
|
neuper@37954
|
170 |
" else (hd rs_)); " ^
|
neuper@37954
|
171 |
" (mx_::real) = " ^
|
neuper@37954
|
172 |
"SubProblem(DiffApp_,[on_interval,maximum_of,function], " ^
|
neuper@37954
|
173 |
" [DiffApp,max_on_interval_by_calculus]) " ^
|
neuper@37984
|
174 |
" [BOOL t_, REAL v_v, REAL_SET itv_] " ^
|
neuper@37954
|
175 |
" in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) " ^
|
neuper@37984
|
176 |
" [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, " ^
|
neuper@37984
|
177 |
" BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) "
|
neuper@37954
|
178 |
));
|
neuper@37954
|
179 |
store_met
|
neuper@37972
|
180 |
(prep_met thy "met_diffapp_funnew" [] e_metID
|
neuper@37954
|
181 |
(["DiffApp","make_fun_by_new_variable"]:metID,
|
neuper@37981
|
182 |
[("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
|
neuper@37954
|
183 |
("#Find" ,["functionEq f_1_"])
|
neuper@37954
|
184 |
],
|
neuper@37954
|
185 |
{rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
|
neuper@37954
|
186 |
calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
|
neuper@37982
|
187 |
"Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^
|
neuper@37954
|
188 |
" (eqs_::bool list) = " ^
|
neuper@37954
|
189 |
"(let h_ = (hd o (filterVar f_)) eqs_; " ^
|
neuper@37954
|
190 |
" es_ = dropWhile (ident h_) eqs_; " ^
|
neuper@37954
|
191 |
" vs_ = dropWhile (ident f_) (Vars h_); " ^
|
neuper@37954
|
192 |
" v_1 = nth_ 1 vs_; " ^
|
neuper@37954
|
193 |
" v_2 = nth_ 2 vs_; " ^
|
neuper@37954
|
194 |
" e_1 = (hd o (filterVar v_1)) es_; " ^
|
neuper@37954
|
195 |
" e_2 = (hd o (filterVar v_2)) es_; " ^
|
neuper@37954
|
196 |
" (s_1::bool list) = " ^
|
neuper@37954
|
197 |
" (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
|
neuper@37984
|
198 |
" [BOOL e_1, REAL v_1]); " ^
|
neuper@37954
|
199 |
" (s_2::bool list) = " ^
|
neuper@37954
|
200 |
" (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^
|
neuper@37984
|
201 |
" [BOOL e_2, REAL v_2])" ^
|
neuper@37954
|
202 |
"in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
|
neuper@37954
|
203 |
));
|
neuper@37954
|
204 |
store_met
|
neuper@37972
|
205 |
(prep_met thy "met_diffapp_funexp" [] e_metID
|
neuper@37954
|
206 |
(["DiffApp","make_fun_by_explicit"]:metID,
|
neuper@37981
|
207 |
[("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
|
neuper@37954
|
208 |
("#Find" ,["functionEq f_1_"])
|
neuper@37954
|
209 |
],
|
neuper@37954
|
210 |
{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
|
neuper@37954
|
211 |
crls = eval_rls, nrls=norm_Rational
|
neuper@37954
|
212 |
(*, asm_rls=[],asm_thm=[]*)},
|
neuper@37982
|
213 |
"Script Make_fun_by_explicit (f_::real) (v_v::real) " ^
|
neuper@37954
|
214 |
" (eqs_::bool list) = " ^
|
neuper@37954
|
215 |
" (let h_ = (hd o (filterVar f_)) eqs_; " ^
|
neuper@37954
|
216 |
" e_1 = hd (dropWhile (ident h_) eqs_); " ^
|
neuper@37954
|
217 |
" vs_ = dropWhile (ident f_) (Vars h_); " ^
|
neuper@37981
|
218 |
" v_1 = hd (dropWhile (ident v_v) vs_); " ^
|
neuper@37954
|
219 |
" (s_1::bool list)= " ^
|
neuper@37954
|
220 |
" (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^
|
neuper@37984
|
221 |
" [BOOL e_1, REAL v_1]) " ^
|
neuper@37954
|
222 |
" in Substitute [(v_1 = (rhs o hd) s_1)] h_) "
|
neuper@37954
|
223 |
));
|
neuper@37954
|
224 |
store_met
|
neuper@37972
|
225 |
(prep_met thy "met_diffapp_max_oninterval" [] e_metID
|
neuper@37954
|
226 |
(["DiffApp","max_on_interval_by_calculus"]:metID,
|
neuper@37981
|
227 |
[("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"(*,
|
neuper@37954
|
228 |
"errorBound err_"*)]),
|
neuper@37954
|
229 |
("#Find" ,["maxArgument v_0_"])
|
neuper@37954
|
230 |
],
|
neuper@37954
|
231 |
{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
|
neuper@37954
|
232 |
crls = eval_rls, nrls=norm_Rational
|
neuper@37954
|
233 |
(*, asm_rls=[],asm_thm=[]*)},
|
neuper@37954
|
234 |
"empty_script"
|
neuper@37954
|
235 |
));
|
neuper@37954
|
236 |
store_met
|
neuper@37972
|
237 |
(prep_met thy "met_diffapp_findvals" [] e_metID
|
neuper@37954
|
238 |
(["DiffApp","find_values"]:metID,
|
neuper@37954
|
239 |
[],
|
neuper@37954
|
240 |
{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
|
neuper@37954
|
241 |
crls = eval_rls, nrls=norm_Rational(*,
|
neuper@37954
|
242 |
asm_rls=[],asm_thm=[]*)},
|
neuper@37954
|
243 |
"empty_script"));
|
neuper@37954
|
244 |
|
neuper@37954
|
245 |
val list_rls = append_rls "list_rls" list_rls
|
neuper@37969
|
246 |
[Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
|
neuper@37969
|
247 |
Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})
|
neuper@37954
|
248 |
];
|
neuper@37967
|
249 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
250 |
[("list_rls",list_rls)
|
neuper@37954
|
251 |
]);
|
neuper@37954
|
252 |
*}
|
neuper@37906
|
253 |
|
neuper@37906
|
254 |
end |