1 (* tools for differentiation |
|
2 WN.11.99 |
|
3 |
|
4 use"IsacKnowledge/Diff.ML"; |
|
5 use"Diff.ML"; |
|
6 *) |
|
7 |
|
8 |
|
9 (** interface isabelle -- isac **) |
|
10 |
|
11 theory' := overwritel (!theory', [("Diff.thy",Diff.thy)]); |
|
12 |
|
13 |
|
14 (** eval functions **) |
|
15 |
|
16 fun primed (Const (id, T)) = Const (id ^ "'", T) |
|
17 | primed (Free (id, T)) = Free (id ^ "'", T) |
|
18 | primed t = raise error ("primed called with arg = '"^ term2str t ^"'"); |
|
19 |
|
20 (*("primed", ("Diff.primed", eval_primed "#primed"))*) |
|
21 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ = |
|
22 SOME ((term2str p) ^ " = " ^ term2str (primed t), |
|
23 Trueprop $ (mk_equality (p, primed t))) |
|
24 | eval_primed _ _ _ _ = NONE; |
|
25 |
|
26 calclist':= overwritel (!calclist', |
|
27 [("primed", ("Diff.primed", eval_primed "#primed")) |
|
28 ]); |
|
29 |
|
30 |
|
31 (** rulesets **) |
|
32 |
|
33 (*.converts a term such that differentiation works optimally.*) |
|
34 val diff_conv = |
|
35 Rls {id="diff_conv", |
|
36 preconds = [], |
|
37 rew_ord = ("termlessI",termlessI), |
|
38 erls = append_rls "erls_diff_conv" e_rls |
|
39 [Calc ("Atools.occurs'_in", eval_occurs_in ""), |
|
40 Thm ("not_true",num_str not_true), |
|
41 Thm ("not_false",num_str not_false), |
|
42 Calc ("op <",eval_equ "#less_"), |
|
43 Thm ("and_true",num_str and_true), |
|
44 Thm ("and_false",num_str and_false) |
|
45 ], |
|
46 srls = Erls, calc = [], |
|
47 rules = [Thm ("frac_conv", num_str frac_conv), |
|
48 Thm ("sqrt_conv_bdv", num_str sqrt_conv_bdv), |
|
49 Thm ("sqrt_conv_bdv_n", num_str sqrt_conv_bdv_n), |
|
50 Thm ("sqrt_conv", num_str sqrt_conv), |
|
51 Thm ("root_conv", num_str root_conv), |
|
52 Thm ("realpow_pow_bdv", num_str realpow_pow_bdv), |
|
53 Calc ("op *", eval_binop "#mult_"), |
|
54 Thm ("rat_mult",num_str rat_mult), |
|
55 (*a / b * (c / d) = a * c / (b * d)*) |
|
56 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq), |
|
57 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
|
58 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq) |
|
59 (*?y / ?z * ?x = ?y * ?x / ?z*) |
|
60 (* |
|
61 Thm ("", num_str ),*) |
|
62 ], |
|
63 scr = EmptyScr}; |
|
64 |
|
65 (*.beautifies a term after differentiation.*) |
|
66 val diff_sym_conv = |
|
67 Rls {id="diff_sym_conv", |
|
68 preconds = [], |
|
69 rew_ord = ("termlessI",termlessI), |
|
70 erls = append_rls "erls_diff_sym_conv" e_rls |
|
71 [Calc ("op <",eval_equ "#less_") |
|
72 ], |
|
73 srls = Erls, calc = [], |
|
74 rules = [Thm ("frac_sym_conv", num_str frac_sym_conv), |
|
75 Thm ("sqrt_sym_conv", num_str sqrt_sym_conv), |
|
76 Thm ("root_sym_conv", num_str root_sym_conv), |
|
77 Thm ("sym_real_mult_minus1", |
|
78 num_str (real_mult_minus1 RS sym)), |
|
79 (*- ?z = "-1 * ?z"*) |
|
80 Thm ("rat_mult",num_str rat_mult), |
|
81 (*a / b * (c / d) = a * c / (b * d)*) |
|
82 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq), |
|
83 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
|
84 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq), |
|
85 (*?y / ?z * ?x = ?y * ?x / ?z*) |
|
86 Calc ("op *", eval_binop "#mult_") |
|
87 ], |
|
88 scr = EmptyScr}; |
|
89 |
|
90 (*..*) |
|
91 val srls_diff = |
|
92 Rls {id="srls_differentiate..", |
|
93 preconds = [], |
|
94 rew_ord = ("termlessI",termlessI), |
|
95 erls = e_rls, |
|
96 srls = Erls, calc = [], |
|
97 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
|
98 Calc("Tools.rhs", eval_rhs "eval_rhs_"), |
|
99 Calc("Diff.primed", eval_primed "Diff.primed") |
|
100 ], |
|
101 scr = EmptyScr}; |
|
102 |
|
103 (*..*) |
|
104 val erls_diff = |
|
105 append_rls "erls_differentiate.." e_rls |
|
106 [Thm ("not_true",num_str not_true), |
|
107 Thm ("not_false",num_str not_false), |
|
108 |
|
109 Calc ("Atools.ident",eval_ident "#ident_"), |
|
110 Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"), |
|
111 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
|
112 Calc ("Atools.is'_const",eval_const "#is_const_") |
|
113 ]; |
|
114 |
|
115 (*.rules for differentiation, _no_ simplification.*) |
|
116 val diff_rules = |
|
117 Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), |
|
118 erls = erls_diff, srls = Erls, calc = [], |
|
119 rules = [Thm ("diff_sum",num_str diff_sum), |
|
120 Thm ("diff_dif",num_str diff_dif), |
|
121 Thm ("diff_prod_const",num_str diff_prod_const), |
|
122 Thm ("diff_prod",num_str diff_prod), |
|
123 Thm ("diff_quot",num_str diff_quot), |
|
124 Thm ("diff_sin",num_str diff_sin), |
|
125 Thm ("diff_sin_chain",num_str diff_sin_chain), |
|
126 Thm ("diff_cos",num_str diff_cos), |
|
127 Thm ("diff_cos_chain",num_str diff_cos_chain), |
|
128 Thm ("diff_pow",num_str diff_pow), |
|
129 Thm ("diff_pow_chain",num_str diff_pow_chain), |
|
130 Thm ("diff_ln",num_str diff_ln), |
|
131 Thm ("diff_ln_chain",num_str diff_ln_chain), |
|
132 Thm ("diff_exp",num_str diff_exp), |
|
133 Thm ("diff_exp_chain",num_str diff_exp_chain), |
|
134 (* |
|
135 Thm ("diff_sqrt",num_str diff_sqrt), |
|
136 Thm ("diff_sqrt_chain",num_str diff_sqrt_chain), |
|
137 *) |
|
138 Thm ("diff_const",num_str diff_const), |
|
139 Thm ("diff_var",num_str diff_var) |
|
140 ], |
|
141 scr = EmptyScr}; |
|
142 |
|
143 (*.normalisation for checking user-input.*) |
|
144 val norm_diff = |
|
145 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), |
|
146 erls = Erls, srls = Erls, calc = [], |
|
147 rules = [Rls_ diff_rules, |
|
148 Rls_ norm_Poly |
|
149 ], |
|
150 scr = EmptyScr}; |
|
151 ruleset' := |
|
152 overwritelthy thy (!ruleset', |
|
153 [("diff_rules", prep_rls norm_diff), |
|
154 ("norm_diff", prep_rls norm_diff), |
|
155 ("diff_conv", prep_rls diff_conv), |
|
156 ("diff_sym_conv", prep_rls diff_sym_conv) |
|
157 ]); |
|
158 |
|
159 |
|
160 (** problem types **) |
|
161 |
|
162 store_pbt |
|
163 (prep_pbt Diff.thy "pbl_fun" [] e_pblID |
|
164 (["function"], [], e_rls, NONE, [])); |
|
165 |
|
166 store_pbt |
|
167 (prep_pbt Diff.thy "pbl_fun_deriv" [] e_pblID |
|
168 (["derivative_of","function"], |
|
169 [("#Given" ,["functionTerm f_","differentiateFor v_"]), |
|
170 ("#Find" ,["derivative f_'_"]) |
|
171 ], |
|
172 append_rls "e_rls" e_rls [], |
|
173 SOME "Diff (f_, v_)", [["diff","differentiate_on_R"], |
|
174 ["diff","after_simplification"]])); |
|
175 |
|
176 (*here "named" is used differently from Integration"*) |
|
177 store_pbt |
|
178 (prep_pbt Diff.thy "pbl_fun_deriv_nam" [] e_pblID |
|
179 (["named","derivative_of","function"], |
|
180 [("#Given" ,["functionEq f_","differentiateFor v_"]), |
|
181 ("#Find" ,["derivativeEq f_'_"]) |
|
182 ], |
|
183 append_rls "e_rls" e_rls [], |
|
184 SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]])); |
|
185 |
|
186 |
|
187 (** methods **) |
|
188 |
|
189 store_met |
|
190 (prep_met Diff.thy "met_diff" [] e_metID |
|
191 (["diff"], [], |
|
192 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
|
193 crls = Atools_erls, nrls = norm_diff}, "empty_script")); |
|
194 |
|
195 store_met |
|
196 (prep_met Diff.thy "met_diff_onR" [] e_metID |
|
197 (["diff","differentiate_on_R"], |
|
198 [("#Given" ,["functionTerm f_","differentiateFor v_"]), |
|
199 ("#Find" ,["derivative f_'_"]) |
|
200 ], |
|
201 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
|
202 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
|
203 "Script DiffScr (f_::real) (v_::real) = \ |
|
204 \ (let f'_ = Take (d_d v_ f_) \ |
|
205 \ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \ |
|
206 \ (Repeat \ |
|
207 \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ |
|
208 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \ |
|
209 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \ |
|
210 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \ |
|
211 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \ |
|
212 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \ |
|
213 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \ |
|
214 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \ |
|
215 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \ |
|
216 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \ |
|
217 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \ |
|
218 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \ |
|
219 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \ |
|
220 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \ |
|
221 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \ |
|
222 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \ |
|
223 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ |
|
224 \ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)" |
|
225 )); |
|
226 |
|
227 store_met |
|
228 (prep_met Diff.thy "met_diff_simpl" [] e_metID |
|
229 (["diff","diff_simpl"], |
|
230 [("#Given" ,["functionTerm f_","differentiateFor v_"]), |
|
231 ("#Find" ,["derivative f_'_"]) |
|
232 ], |
|
233 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
|
234 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
|
235 "Script DiffScr (f_::real) (v_::real) = \ |
|
236 \ (let f'_ = Take (d_d v_ f_) \ |
|
237 \ in (( \ |
|
238 \ (Repeat \ |
|
239 \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ |
|
240 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \ |
|
241 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \ |
|
242 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \ |
|
243 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \ |
|
244 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \ |
|
245 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \ |
|
246 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \ |
|
247 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \ |
|
248 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \ |
|
249 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \ |
|
250 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \ |
|
251 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \ |
|
252 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \ |
|
253 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \ |
|
254 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \ |
|
255 \ (Repeat (Rewrite_Set make_polynomial False)))) \ |
|
256 \ )) f'_)" |
|
257 )); |
|
258 |
|
259 (*----------------------------------------------------------------- |
|
260 "Script DiffScr (f_::real) (v_::real) = \ |
|
261 \(Repeat \ |
|
262 \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ |
|
263 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \ |
|
264 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \ |
|
265 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \ |
|
266 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \ |
|
267 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \ |
|
268 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \ |
|
269 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \ |
|
270 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \ |
|
271 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \ |
|
272 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \ |
|
273 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \ |
|
274 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \ |
|
275 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \ |
|
276 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \ |
|
277 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \ |
|
278 \ (Repeat (Rewrite_Set make_polynomial False)))) \ |
|
279 \ (f_::real)" |
|
280 *) |
|
281 |
|
282 store_met |
|
283 (prep_met Diff.thy "met_diff_equ" [] e_metID |
|
284 (["diff","differentiate_equality"], |
|
285 [("#Given" ,["functionEq f_","differentiateFor v_"]), |
|
286 ("#Find" ,["derivativeEq f_'_"]) |
|
287 ], |
|
288 {rew_ord'="tless_true", rls' = erls_diff, calc = [], |
|
289 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff}, |
|
290 "Script DiffEqScr (f_::bool) (v_::real) = \ |
|
291 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) \ |
|
292 \ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \ |
|
293 \ (Repeat \ |
|
294 \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ |
|
295 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or \ |
|
296 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \ |
|
297 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \ |
|
298 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \ |
|
299 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \ |
|
300 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \ |
|
301 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \ |
|
302 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \ |
|
303 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \ |
|
304 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \ |
|
305 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \ |
|
306 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \ |
|
307 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \ |
|
308 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \ |
|
309 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \ |
|
310 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \ |
|
311 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ |
|
312 \ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)" |
|
313 )); |
|
314 |
|
315 |
|
316 store_met |
|
317 (prep_met Diff.thy "met_diff_after_simp" [] e_metID |
|
318 (["diff","after_simplification"], |
|
319 [("#Given" ,["functionTerm f_","differentiateFor v_"]), |
|
320 ("#Find" ,["derivative f_'_"]) |
|
321 ], |
|
322 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls, |
|
323 crls=Atools_erls, nrls = norm_Rational}, |
|
324 "Script DiffScr (f_::real) (v_::real) = \ |
|
325 \ (let f'_ = Take (d_d v_ f_) \ |
|
326 \ in ((Try (Rewrite_Set norm_Rational False)) @@ \ |
|
327 \ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \ |
|
328 \ (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ \ |
|
329 \ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ \ |
|
330 \ (Try (Rewrite_Set norm_Rational False))) f'_)" |
|
331 )); |
|
332 |
|
333 |
|
334 (** CAS-commands **) |
|
335 |
|
336 (*.handle cas-input like "Diff (a * x^3 + b, x)".*) |
|
337 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)"); |
|
338 val [Const ("Pair", _) $ t $ bdv] = pairl; |
|
339 *) |
|
340 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
|
341 [((term_of o the o (parse thy)) "functionTerm", [t]), |
|
342 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
|
343 ((term_of o the o (parse thy)) "derivative", |
|
344 [(term_of o the o (parse thy)) "f_'_"]) |
|
345 ] |
|
346 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
|
347 castab := |
|
348 overwritel (!castab, |
|
349 [((term_of o the o (parse thy)) "Diff", |
|
350 (("Isac.thy", ["derivative_of","function"], ["no_met"]), |
|
351 argl2dtss)) |
|
352 ]); |
|
353 |
|
354 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) |
|
355 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)"); |
|
356 val [Const ("Pair", _) $ t $ bdv] = pairl; |
|
357 *) |
|
358 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
|
359 [((term_of o the o (parse thy)) "functionEq", [t]), |
|
360 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
|
361 ((term_of o the o (parse thy)) "derivativeEq", |
|
362 [(term_of o the o (parse thy)) "f_'_::bool"]) |
|
363 ] |
|
364 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
|
365 castab := |
|
366 overwritel (!castab, |
|
367 [((term_of o the o (parse thy)) "Differentiate", |
|
368 (("Isac.thy", ["named","derivative_of","function"], ["no_met"]), |
|
369 argl2dtss)) |
|
370 ]); |
|