1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/IsacKnowledge/Diff.ML Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,370 @@
1.4 +(* tools for differentiation
1.5 + WN.11.99
1.6 +
1.7 +use"IsacKnowledge/Diff.ML";
1.8 +use"Diff.ML";
1.9 + *)
1.10 +
1.11 +
1.12 +(** interface isabelle -- isac **)
1.13 +
1.14 +theory' := overwritel (!theory', [("Diff.thy",Diff.thy)]);
1.15 +
1.16 +
1.17 +(** eval functions **)
1.18 +
1.19 +fun primed (Const (id, T)) = Const (id ^ "'", T)
1.20 + | primed (Free (id, T)) = Free (id ^ "'", T)
1.21 + | primed t = raise error ("primed called with arg = '"^ term2str t ^"'");
1.22 +
1.23 +(*("primed", ("Diff.primed", eval_primed "#primed"))*)
1.24 +fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
1.25 + Some ((term2str p) ^ " = " ^ term2str (primed t),
1.26 + Trueprop $ (mk_equality (p, primed t)))
1.27 + | eval_primed _ _ _ _ = None;
1.28 +
1.29 +calclist':= overwritel (!calclist',
1.30 + [("primed", ("Diff.primed", eval_primed "#primed"))
1.31 + ]);
1.32 +
1.33 +
1.34 +(** rulesets **)
1.35 +
1.36 +(*.converts a term such that differentiation works optimally.*)
1.37 +val diff_conv =
1.38 + Rls {id="diff_conv",
1.39 + preconds = [],
1.40 + rew_ord = ("termlessI",termlessI),
1.41 + erls = append_rls "erls_diff_conv" e_rls
1.42 + [Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.43 + Thm ("not_true",num_str not_true),
1.44 + Thm ("not_false",num_str not_false),
1.45 + Calc ("op <",eval_equ "#less_"),
1.46 + Thm ("and_true",num_str and_true),
1.47 + Thm ("and_false",num_str and_false)
1.48 + ],
1.49 + srls = Erls, calc = [],
1.50 + rules = [Thm ("frac_conv", num_str frac_conv),
1.51 + Thm ("sqrt_conv_bdv", num_str sqrt_conv_bdv),
1.52 + Thm ("sqrt_conv_bdv_n", num_str sqrt_conv_bdv_n),
1.53 + Thm ("sqrt_conv", num_str sqrt_conv),
1.54 + Thm ("root_conv", num_str root_conv),
1.55 + Thm ("realpow_pow_bdv", num_str realpow_pow_bdv),
1.56 + Calc ("op *", eval_binop "#mult_"),
1.57 + Thm ("rat_mult",num_str rat_mult),
1.58 + (*a / b * (c / d) = a * c / (b * d)*)
1.59 + Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
1.60 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.61 + Thm ("real_times_divide2_eq",num_str real_times_divide2_eq)
1.62 + (*?y / ?z * ?x = ?y * ?x / ?z*)
1.63 + (*
1.64 + Thm ("", num_str ),*)
1.65 + ],
1.66 + scr = EmptyScr};
1.67 +
1.68 +(*.beautifies a term after differentiation.*)
1.69 +val diff_sym_conv =
1.70 + Rls {id="diff_sym_conv",
1.71 + preconds = [],
1.72 + rew_ord = ("termlessI",termlessI),
1.73 + erls = append_rls "erls_diff_sym_conv" e_rls
1.74 + [Calc ("op <",eval_equ "#less_")
1.75 + ],
1.76 + srls = Erls, calc = [],
1.77 + rules = [Thm ("frac_sym_conv", num_str frac_sym_conv),
1.78 + Thm ("sqrt_sym_conv", num_str sqrt_sym_conv),
1.79 + Thm ("root_sym_conv", num_str root_sym_conv),
1.80 + Thm ("sym_real_mult_minus1",
1.81 + num_str (real_mult_minus1 RS sym)),
1.82 + (*- ?z = "-1 * ?z"*)
1.83 + Thm ("rat_mult",num_str rat_mult),
1.84 + (*a / b * (c / d) = a * c / (b * d)*)
1.85 + Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
1.86 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.87 + Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
1.88 + (*?y / ?z * ?x = ?y * ?x / ?z*)
1.89 + Calc ("op *", eval_binop "#mult_")
1.90 + ],
1.91 + scr = EmptyScr};
1.92 +
1.93 +(*..*)
1.94 +val srls_diff =
1.95 + Rls {id="srls_differentiate..",
1.96 + preconds = [],
1.97 + rew_ord = ("termlessI",termlessI),
1.98 + erls = e_rls,
1.99 + srls = Erls, calc = [],
1.100 + rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.101 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.102 + Calc("Diff.primed", eval_primed "Diff.primed")
1.103 + ],
1.104 + scr = EmptyScr};
1.105 +
1.106 +(*..*)
1.107 +val erls_diff =
1.108 + append_rls "erls_differentiate.." e_rls
1.109 + [Thm ("not_true",num_str not_true),
1.110 + Thm ("not_false",num_str not_false),
1.111 +
1.112 + Calc ("Atools.ident",eval_ident "#ident_"),
1.113 + Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.114 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.115 + Calc ("Atools.is'_const",eval_const "#is_const_")
1.116 + ];
1.117 +
1.118 +(*.rules for differentiation, _no_ simplification.*)
1.119 +val diff_rules =
1.120 + Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
1.121 + erls = erls_diff, srls = Erls, calc = [],
1.122 + rules = [Thm ("diff_sum",num_str diff_sum),
1.123 + Thm ("diff_dif",num_str diff_dif),
1.124 + Thm ("diff_prod_const",num_str diff_prod_const),
1.125 + Thm ("diff_prod",num_str diff_prod),
1.126 + Thm ("diff_quot",num_str diff_quot),
1.127 + Thm ("diff_sin",num_str diff_sin),
1.128 + Thm ("diff_sin_chain",num_str diff_sin_chain),
1.129 + Thm ("diff_cos",num_str diff_cos),
1.130 + Thm ("diff_cos_chain",num_str diff_cos_chain),
1.131 + Thm ("diff_pow",num_str diff_pow),
1.132 + Thm ("diff_pow_chain",num_str diff_pow_chain),
1.133 + Thm ("diff_ln",num_str diff_ln),
1.134 + Thm ("diff_ln_chain",num_str diff_ln_chain),
1.135 + Thm ("diff_exp",num_str diff_exp),
1.136 + Thm ("diff_exp_chain",num_str diff_exp_chain),
1.137 +(*
1.138 + Thm ("diff_sqrt",num_str diff_sqrt),
1.139 + Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),
1.140 +*)
1.141 + Thm ("diff_const",num_str diff_const),
1.142 + Thm ("diff_var",num_str diff_var)
1.143 + ],
1.144 + scr = EmptyScr};
1.145 +
1.146 +(*.normalisation for checking user-input.*)
1.147 +val norm_diff =
1.148 + Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
1.149 + erls = Erls, srls = Erls, calc = [],
1.150 + rules = [Rls_ diff_rules,
1.151 + Rls_ norm_Poly
1.152 + ],
1.153 + scr = EmptyScr};
1.154 +ruleset' :=
1.155 +overwritelthy thy (!ruleset',
1.156 + [("diff_rules", prep_rls norm_diff),
1.157 + ("norm_diff", prep_rls norm_diff),
1.158 + ("diff_conv", prep_rls diff_conv),
1.159 + ("diff_sym_conv", prep_rls diff_sym_conv)
1.160 + ]);
1.161 +
1.162 +
1.163 +(** problem types **)
1.164 +
1.165 +store_pbt
1.166 + (prep_pbt Diff.thy "pbl_fun" [] e_pblID
1.167 + (["function"], [], e_rls, None, []));
1.168 +
1.169 +store_pbt
1.170 + (prep_pbt Diff.thy "pbl_fun_deriv" [] e_pblID
1.171 + (["derivative_of","function"],
1.172 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.173 + ("#Find" ,["derivative f_'_"])
1.174 + ],
1.175 + append_rls "e_rls" e_rls [],
1.176 + Some "Diff (f_, v_)", [["diff","differentiate_on_R"],
1.177 + ["diff","after_simplification"]]));
1.178 +
1.179 +(*here "named" is used differently from Integration"*)
1.180 +store_pbt
1.181 + (prep_pbt Diff.thy "pbl_fun_deriv_nam" [] e_pblID
1.182 + (["named","derivative_of","function"],
1.183 + [("#Given" ,["functionEq f_","differentiateFor v_"]),
1.184 + ("#Find" ,["derivativeEq f_'_"])
1.185 + ],
1.186 + append_rls "e_rls" e_rls [],
1.187 + Some "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));
1.188 +
1.189 +
1.190 +(** methods **)
1.191 +
1.192 +store_met
1.193 + (prep_met Diff.thy "met_diff" [] e_metID
1.194 + (["diff"], [],
1.195 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.196 + crls = Atools_erls, nrls = norm_diff}, "empty_script"));
1.197 +
1.198 +store_met
1.199 + (prep_met Diff.thy "met_diff_onR" [] e_metID
1.200 + (["diff","differentiate_on_R"],
1.201 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.202 + ("#Find" ,["derivative f_'_"])
1.203 + ],
1.204 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.205 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.206 +"Script DiffScr (f_::real) (v_::real) = \
1.207 +\ (let f'_ = Take (d_d v_ f_) \
1.208 +\ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \
1.209 +\ (Repeat \
1.210 +\ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
1.211 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
1.212 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
1.213 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
1.214 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
1.215 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
1.216 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
1.217 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
1.218 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
1.219 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
1.220 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
1.221 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
1.222 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
1.223 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
1.224 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
1.225 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
1.226 +\ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
1.227 +\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.228 +));
1.229 +
1.230 +store_met
1.231 + (prep_met Diff.thy "met_diff_simpl" [] e_metID
1.232 + (["diff","diff_simpl"],
1.233 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.234 + ("#Find" ,["derivative f_'_"])
1.235 + ],
1.236 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.237 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.238 +"Script DiffScr (f_::real) (v_::real) = \
1.239 +\ (let f'_ = Take (d_d v_ f_) \
1.240 +\ in (( \
1.241 +\ (Repeat \
1.242 +\ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
1.243 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
1.244 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
1.245 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
1.246 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
1.247 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
1.248 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
1.249 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
1.250 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
1.251 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
1.252 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
1.253 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
1.254 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
1.255 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
1.256 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
1.257 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
1.258 +\ (Repeat (Rewrite_Set make_polynomial False)))) \
1.259 +\ )) f'_)"
1.260 + ));
1.261 +
1.262 +(*-----------------------------------------------------------------
1.263 + "Script DiffScr (f_::real) (v_::real) = \
1.264 + \(Repeat \
1.265 + \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
1.266 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
1.267 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
1.268 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
1.269 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
1.270 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
1.271 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
1.272 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
1.273 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
1.274 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
1.275 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
1.276 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
1.277 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
1.278 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
1.279 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
1.280 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
1.281 + \ (Repeat (Rewrite_Set make_polynomial False)))) \
1.282 + \ (f_::real)"
1.283 +*)
1.284 +
1.285 +store_met
1.286 + (prep_met Diff.thy "met_diff_equ" [] e_metID
1.287 + (["diff","differentiate_equality"],
1.288 + [("#Given" ,["functionEq f_","differentiateFor v_"]),
1.289 + ("#Find" ,["derivativeEq f_'_"])
1.290 + ],
1.291 + {rew_ord'="tless_true", rls' = erls_diff, calc = [],
1.292 + srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
1.293 +"Script DiffEqScr (f_::bool) (v_::real) = \
1.294 +\ (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) \
1.295 +\ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \
1.296 +\ (Repeat \
1.297 +\ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
1.298 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or \
1.299 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
1.300 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
1.301 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
1.302 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
1.303 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
1.304 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
1.305 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
1.306 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
1.307 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
1.308 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
1.309 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
1.310 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
1.311 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
1.312 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
1.313 +\ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
1.314 +\ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
1.315 +\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.316 +));
1.317 +
1.318 +
1.319 +store_met
1.320 + (prep_met Diff.thy "met_diff_after_simp" [] e_metID
1.321 + (["diff","after_simplification"],
1.322 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.323 + ("#Find" ,["derivative f_'_"])
1.324 + ],
1.325 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
1.326 + crls=Atools_erls, nrls = norm_Rational},
1.327 +"Script DiffScr (f_::real) (v_::real) = \
1.328 +\ (let f'_ = Take (d_d v_ f_) \
1.329 +\ in ((Try (Rewrite_Set norm_Rational False)) @@ \
1.330 +\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \
1.331 +\ (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ \
1.332 +\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ \
1.333 +\ (Try (Rewrite_Set norm_Rational False))) f'_)"
1.334 +));
1.335 +
1.336 +
1.337 +(** CAS-commands **)
1.338 +
1.339 +(*.handle cas-input like "Diff (a * x^3 + b, x)".*)
1.340 +(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
1.341 + val [Const ("Pair", _) $ t $ bdv] = pairl;
1.342 + *)
1.343 +fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
1.344 + [((term_of o the o (parse thy)) "functionTerm", [t]),
1.345 + ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
1.346 + ((term_of o the o (parse thy)) "derivative",
1.347 + [(term_of o the o (parse thy)) "f_'_"])
1.348 + ]
1.349 + | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
1.350 +castab :=
1.351 +overwritel (!castab,
1.352 + [((term_of o the o (parse thy)) "Diff",
1.353 + (("Isac.thy", ["derivative_of","function"], ["no_met"]),
1.354 + argl2dtss))
1.355 + ]);
1.356 +
1.357 +(*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
1.358 +(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
1.359 + val [Const ("Pair", _) $ t $ bdv] = pairl;
1.360 + *)
1.361 +fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
1.362 + [((term_of o the o (parse thy)) "functionEq", [t]),
1.363 + ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
1.364 + ((term_of o the o (parse thy)) "derivativeEq",
1.365 + [(term_of o the o (parse thy)) "f_'_::bool"])
1.366 + ]
1.367 + | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
1.368 +castab :=
1.369 +overwritel (!castab,
1.370 + [((term_of o the o (parse thy)) "Differentiate",
1.371 + (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),
1.372 + argl2dtss))
1.373 + ]);