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