1 (* tools for differentiation
4 use"IsacKnowledge/Diff.ML";
9 (** interface isabelle -- isac **)
11 theory' := overwritel (!theory', [("Diff.thy",Diff.thy)]);
14 (** eval functions **)
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 ^"'");
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;
26 calclist':= overwritel (!calclist',
27 [("primed", ("Diff.primed", eval_primed "#primed"))
33 (*.converts a term such that differentiation works optimally.*)
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)
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*)
65 (*.beautifies a term after differentiation.*)
67 Rls {id="diff_sym_conv",
69 rew_ord = ("termlessI",termlessI),
70 erls = append_rls "erls_diff_sym_conv" e_rls
71 [Calc ("op <",eval_equ "#less_")
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)),
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_")
92 Rls {id="srls_differentiate..",
94 rew_ord = ("termlessI",termlessI),
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")
105 append_rls "erls_differentiate.." e_rls
106 [Thm ("not_true",num_str not_true),
107 Thm ("not_false",num_str not_false),
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_")
115 (*.rules for differentiation, _no_ simplification.*)
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),
135 Thm ("diff_sqrt",num_str diff_sqrt),
136 Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),
138 Thm ("diff_const",num_str diff_const),
139 Thm ("diff_var",num_str diff_var)
143 (*.normalisation for checking user-input.*)
145 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
146 erls = Erls, srls = Erls, calc = [],
147 rules = [Rls_ diff_rules,
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)
160 (** problem types **)
163 (prep_pbt Diff.thy "pbl_fun" [] e_pblID
164 (["function"], [], e_rls, NONE, []));
167 (prep_pbt Diff.thy "pbl_fun_deriv" [] e_pblID
168 (["derivative_of","function"],
169 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
170 ("#Find" ,["derivative f_'_"])
172 append_rls "e_rls" e_rls [],
173 SOME "Diff (f_, v_)", [["diff","differentiate_on_R"],
174 ["diff","after_simplification"]]));
176 (*here "named" is used differently from Integration"*)
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_'_"])
183 append_rls "e_rls" e_rls [],
184 SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));
190 (prep_met Diff.thy "met_diff" [] e_metID
192 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
193 crls = Atools_erls, nrls = norm_diff}, "empty_script"));
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_'_"])
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)) @@ \
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'_)"
228 (prep_met Diff.thy "met_diff_simpl" [] e_metID
229 (["diff","diff_simpl"],
230 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
231 ("#Find" ,["derivative f_'_"])
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_) \
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)))) \
259 (*-----------------------------------------------------------------
260 "Script DiffScr (f_::real) (v_::real) = \
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)))) \
283 (prep_met Diff.thy "met_diff_equ" [] e_metID
284 (["diff","differentiate_equality"],
285 [("#Given" ,["functionEq f_","differentiateFor v_"]),
286 ("#Find" ,["derivativeEq f_'_"])
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)) @@ \
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'_)"
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_'_"])
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'_)"
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;
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_'_"])
346 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
349 [((term_of o the o (parse thy)) "Diff",
350 (("Isac.thy", ["derivative_of","function"], ["no_met"]),
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;
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"])
364 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
367 [((term_of o the o (parse thy)) "Differentiate",
368 (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),