|
neuper@37906
|
1 |
(* application of differential calculus
|
|
neuper@37947
|
2 |
use_thy_only"../Knowledge/DiffApp";
|
|
neuper@37906
|
3 |
use_thy_only"DiffApp";
|
|
neuper@37906
|
4 |
|
|
neuper@37906
|
5 |
|
|
neuper@37906
|
6 |
*)
|
|
neuper@37906
|
7 |
|
|
neuper@37906
|
8 |
|
|
neuper@37906
|
9 |
DiffApp = Diff +
|
|
neuper@37906
|
10 |
|
|
neuper@37906
|
11 |
consts
|
|
neuper@37906
|
12 |
|
|
neuper@37906
|
13 |
Maximum'_value
|
|
neuper@37906
|
14 |
:: "[bool list,real,bool list,real,real set,bool,\
|
|
neuper@37906
|
15 |
\ bool list] => bool list"
|
|
neuper@37906
|
16 |
("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
|
|
neuper@37906
|
17 |
|
|
neuper@37906
|
18 |
Make'_fun'_by'_new'_variable
|
|
neuper@37906
|
19 |
:: "[real,real,bool list, \
|
|
neuper@37906
|
20 |
\ bool] => bool"
|
|
neuper@37906
|
21 |
("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// \
|
|
neuper@37906
|
22 |
\(_))" 9)
|
|
neuper@37906
|
23 |
Make'_fun'_by'_explicit
|
|
neuper@37906
|
24 |
:: "[real,real,bool list, \
|
|
neuper@37906
|
25 |
\ bool] => bool"
|
|
neuper@37906
|
26 |
("((Script Make'_fun'_by'_explicit (_ _ _ =))// \
|
|
neuper@37906
|
27 |
\(_))" 9)
|
|
neuper@37906
|
28 |
|
|
neuper@37906
|
29 |
dummy :: real
|
|
neuper@37906
|
30 |
|
|
neuper@37906
|
31 |
(*for script Maximum_value*)
|
|
neuper@37906
|
32 |
filterVar :: "[real, 'a list] => 'a list"
|
|
neuper@37906
|
33 |
|
|
neuper@37906
|
34 |
(*primrec*)rules
|
|
neuper@37906
|
35 |
filterVar_Nil "filterVar v [] = []"
|
|
neuper@37906
|
36 |
filterVar_Const "filterVar v (x#xs) = \
|
|
neuper@37906
|
37 |
\(if (v mem (Vars x)) then x#(filterVar v xs) \
|
|
neuper@37906
|
38 |
\ else filterVar v xs) "
|
|
neuper@37906
|
39 |
|
|
neuper@37906
|
40 |
end |