neuper@37906: (* differentiation over the reals neuper@37906: author: Walther Neuper neuper@37906: 000516 neuper@37906: *) neuper@37906: neuper@37954: theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin neuper@37906: neuper@37993: ML {* neuper@37993: @{term "sin x"} neuper@37993: *} neuper@37993: neuper@37906: consts neuper@37906: neuper@37906: d_d :: "[real, real]=> real" neuper@37993: (*sin, cos :: "real => real" already in Isabelle2009-2*) neuper@37906: (* neuper@37906: log, ln :: "real => real" neuper@37906: nlog :: "[real, real] => real" neuper@37906: exp :: "real => real" ("E'_ ^^^ _" 80) neuper@37906: *) neuper@37906: (*descriptions in the related problems*) neuper@37993: derivativeEq :: "bool => una" neuper@37906: neuper@37906: (*predicates*) neuper@37906: primed :: "'a => 'a" (*"primed A" -> "A'"*) neuper@37906: neuper@37906: (*the CAS-commands, eg. "Diff (2*x^^^3, x)", neuper@37906: "Differentiate (A = s * (a - s), s)"*) neuper@37906: Diff :: "[real * real] => real" neuper@37906: Differentiate :: "[bool * real] => bool" neuper@37906: neuper@37906: (*subproblem and script-name*) neuper@37906: differentiate :: "[ID * (ID list) * ID, real,real] => real" neuper@37906: ("(differentiate (_)/ (_ _ ))" 9) neuper@37906: DiffScr :: "[real,real, real] => real" neuper@37906: ("((Script DiffScr (_ _ =))// (_))" 9) neuper@37993: DiffEqScr :: "[bool,real, bool] => bool" neuper@37906: ("((Script DiffEqScr (_ _ =))// (_))" 9) neuper@37906: neuper@37954: text {*a variant of the derivatives defintion: neuper@37906: neuper@37954: d_d :: "(real => real) => (real => real)" neuper@37954: neuper@37954: advantages: neuper@37954: (1) no variable 'bdv' on the meta-level required neuper@37954: (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v" neuper@37954: (3) and no specialized chain-rules required like neuper@37954: diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u" neuper@37954: neuper@37954: disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation neuper@37954: *} neuper@37954: neuper@37954: axioms (*stated as axioms, todo: prove as theorems neuper@37906: 'bdv' is a constant on the meta-level *) neuper@37983: diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" neuper@37983: diff_var: "d_d bdv bdv = 1" neuper@37983: diff_prod_const:"[| Not (bdv occurs_in u) |] ==> neuper@37954: d_d bdv (u * v) = u * d_d bdv v" neuper@37906: neuper@37983: diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" neuper@37983: diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" neuper@37983: diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" neuper@37983: diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) = neuper@37954: (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" neuper@37906: neuper@37983: diff_sin: "d_d bdv (sin bdv) = cos bdv" neuper@37983: diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" neuper@37983: diff_cos: "d_d bdv (cos bdv) = - sin bdv" neuper@37983: diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" neuper@37983: diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" neuper@37983: diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" neuper@37983: diff_ln: "d_d bdv (ln bdv) = 1 / bdv" neuper@37983: diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" neuper@37983: diff_exp: "d_d bdv (exp bdv) = exp bdv" neuper@37983: diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" neuper@37906: (* neuper@37906: diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)" neuper@37906: diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)" neuper@37906: *) neuper@37906: (*...*) neuper@37906: neuper@37983: frac_conv: "[| bdv occurs_in b; 0 < n |] ==> neuper@37954: a / (b ^^^ n) = a * b ^^^ (-n)" neuper@37983: frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" neuper@37906: neuper@37983: sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" neuper@37983: sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" neuper@37983: sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" neuper@37983: sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" neuper@37906: neuper@37983: root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" neuper@37983: root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" neuper@37906: neuper@37983: realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" neuper@37906: neuper@37954: ML {* neuper@37972: val thy = @{theory}; neuper@37972: neuper@37954: (** eval functions **) neuper@37954: neuper@37954: fun primed (Const (id, T)) = Const (id ^ "'", T) neuper@37954: | primed (Free (id, T)) = Free (id ^ "'", T) neuper@38031: | primed t = error ("primed called with arg = '"^ term2str t ^"'"); neuper@37954: neuper@37954: (*("primed", ("Diff.primed", eval_primed "#primed"))*) neuper@37954: fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ = neuper@37954: SOME ((term2str p) ^ " = " ^ term2str (primed t), neuper@37954: Trueprop $ (mk_equality (p, primed t))) neuper@37954: | eval_primed _ _ _ _ = NONE; neuper@37954: neuper@37954: calclist':= overwritel (!calclist', neuper@37954: [("primed", ("Diff.primed", eval_primed "#primed")) neuper@37954: ]); neuper@37993: *} neuper@37993: ML {* neuper@37954: (** rulesets **) neuper@37954: neuper@37954: (*.converts a term such that differentiation works optimally.*) neuper@37954: val diff_conv = neuper@37954: Rls {id="diff_conv", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), neuper@37954: erls = append_rls "erls_diff_conv" e_rls neuper@37954: [Calc ("Atools.occurs'_in", eval_occurs_in ""), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false}), neuper@37954: Calc ("op <",eval_equ "#less_"), neuper@37969: Thm ("and_true",num_str @{thm and_true}), neuper@37993: Thm ("and_false",num_str @{thm and_false}) neuper@37954: ], neuper@37954: srls = Erls, calc = [], neuper@37969: rules = [Thm ("frac_conv", num_str @{thm frac_conv}), neuper@37969: Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}), neuper@37969: Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}), neuper@37969: Thm ("sqrt_conv", num_str @{thm sqrt_conv}), neuper@37969: Thm ("root_conv", num_str @{thm root_conv}), neuper@37969: Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}), neuper@37954: Calc ("op *", eval_binop "#mult_"), neuper@37969: Thm ("rat_mult",num_str @{thm rat_mult}), neuper@37954: (*a / b * (c / d) = a * c / (b * d)*) neuper@37965: Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), neuper@37954: (*?x * (?y / ?z) = ?x * ?y / ?z*) neuper@37965: Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) neuper@37954: (*?y / ?z * ?x = ?y * ?x / ?z*) neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37993: *} neuper@37993: ML {* neuper@37954: (*.beautifies a term after differentiation.*) neuper@37954: val diff_sym_conv = neuper@37954: Rls {id="diff_sym_conv", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), neuper@37954: erls = append_rls "erls_diff_sym_conv" e_rls neuper@37954: [Calc ("op <",eval_equ "#less_") neuper@37954: ], neuper@37954: srls = Erls, calc = [], neuper@37969: rules = [Thm ("frac_sym_conv", num_str @{thm frac_sym_conv}), neuper@37969: Thm ("sqrt_sym_conv", num_str @{thm sqrt_sym_conv}), neuper@37969: Thm ("root_sym_conv", num_str @{thm root_sym_conv}), neuper@37954: Thm ("sym_real_mult_minus1", neuper@37969: num_str (@{thm real_mult_minus1} RS @{thm sym})), neuper@37954: (*- ?z = "-1 * ?z"*) neuper@37969: Thm ("rat_mult",num_str @{thm rat_mult}), neuper@37954: (*a / b * (c / d) = a * c / (b * d)*) neuper@37965: Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), neuper@37954: (*?x * (?y / ?z) = ?x * ?y / ?z*) neuper@37965: Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), neuper@37954: (*?y / ?z * ?x = ?y * ?x / ?z*) neuper@37954: Calc ("op *", eval_binop "#mult_") neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37954: neuper@37954: (*..*) neuper@37954: val srls_diff = neuper@37954: Rls {id="srls_differentiate..", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), neuper@37954: erls = e_rls, neuper@37954: srls = Erls, calc = [], neuper@37954: rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"), neuper@37954: Calc("Tools.rhs", eval_rhs "eval_rhs_"), neuper@37954: Calc("Diff.primed", eval_primed "Diff.primed") neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37993: *} neuper@37993: ML {* neuper@37954: (*..*) neuper@37954: val erls_diff = neuper@37954: append_rls "erls_differentiate.." e_rls neuper@37969: [Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false}), neuper@37954: neuper@37954: Calc ("Atools.ident",eval_ident "#ident_"), neuper@37954: Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"), neuper@37954: Calc ("Atools.occurs'_in",eval_occurs_in ""), neuper@37954: Calc ("Atools.is'_const",eval_const "#is_const_") neuper@37954: ]; neuper@37954: neuper@37954: (*.rules for differentiation, _no_ simplification.*) neuper@37954: val diff_rules = neuper@37954: Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), neuper@37954: erls = erls_diff, srls = Erls, calc = [], neuper@37969: rules = [Thm ("diff_sum",num_str @{thm diff_sum}), neuper@37969: Thm ("diff_dif",num_str @{thm diff_dif}), neuper@37969: Thm ("diff_prod_const",num_str @{thm diff_prod_const}), neuper@37969: Thm ("diff_prod",num_str @{thm diff_prod}), neuper@37969: Thm ("diff_quot",num_str @{thm diff_quot}), neuper@37969: Thm ("diff_sin",num_str @{thm diff_sin}), neuper@37969: Thm ("diff_sin_chain",num_str @{thm diff_sin_chain}), neuper@37969: Thm ("diff_cos",num_str @{thm diff_cos}), neuper@37969: Thm ("diff_cos_chain",num_str @{thm diff_cos_chain}), neuper@37969: Thm ("diff_pow",num_str @{thm diff_pow}), neuper@37969: Thm ("diff_pow_chain",num_str @{thm diff_pow_chain}), neuper@37969: Thm ("diff_ln",num_str @{thm diff_ln}), neuper@37969: Thm ("diff_ln_chain",num_str @{thm diff_ln_chain}), neuper@37969: Thm ("diff_exp",num_str @{thm diff_exp}), neuper@37969: Thm ("diff_exp_chain",num_str @{thm diff_exp_chain}), neuper@37954: (* neuper@37969: Thm ("diff_sqrt",num_str @{thm diff_sqrt}), neuper@37969: Thm ("diff_sqrt_chain",num_str @{thm diff_sqrt_chain}), neuper@37954: *) neuper@37969: Thm ("diff_const",num_str @{thm diff_const}), neuper@37969: Thm ("diff_var",num_str @{thm diff_var}) neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37993: *} neuper@37993: ML {* neuper@37954: (*.normalisation for checking user-input.*) neuper@37954: val norm_diff = neuper@37954: Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), neuper@37954: erls = Erls, srls = Erls, calc = [], neuper@37954: rules = [Rls_ diff_rules, neuper@37954: Rls_ norm_Poly neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37954: ruleset' := neuper@37967: overwritelthy @{theory} (!ruleset', neuper@37954: [("diff_rules", prep_rls norm_diff), neuper@37954: ("norm_diff", prep_rls norm_diff), neuper@37954: ("diff_conv", prep_rls diff_conv), neuper@37954: ("diff_sym_conv", prep_rls diff_sym_conv) neuper@37954: ]); neuper@37954: neuper@37993: *} neuper@37993: ML {* neuper@37954: (** problem types **) neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun" [] e_pblID neuper@37954: (["function"], [], e_rls, NONE, [])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_deriv" [] e_pblID neuper@37954: (["derivative_of","function"], neuper@37993: [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivative f_f'"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [], neuper@37993: SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"], neuper@37954: ["diff","after_simplification"]])); neuper@37954: neuper@37954: (*here "named" is used differently from Integration"*) neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID neuper@37954: (["named","derivative_of","function"], neuper@37993: [("#Given" ,["functionEq f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivativeEq f_f'"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [], neuper@37993: SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]])); neuper@37993: *} neuper@37993: ML {* neuper@37954: neuper@37954: (** methods **) neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_diff" [] e_metID neuper@37954: (["diff"], [], neuper@37954: {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, neuper@37954: crls = Atools_erls, nrls = norm_diff}, "empty_script")); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_diff_onR" [] e_metID neuper@37954: (["diff","differentiate_on_R"], neuper@37993: [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivative f_f'"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, neuper@37954: prls=e_rls, crls = Atools_erls, nrls = norm_diff}, neuper@37993: "Script DiffScr (f_f::real) (v_v::real) = " ^ neuper@37993: " (let f_f' = Take (d_d v_v f_f) " ^ neuper@37991: " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ neuper@37954: " (Repeat " ^ neuper@37991: " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ neuper@37954: " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ neuper@37993: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')" neuper@37954: )); neuper@37993: *} neuper@37993: ML {* neuper@37954: store_met neuper@37972: (prep_met thy "met_diff_simpl" [] e_metID neuper@37954: (["diff","diff_simpl"], neuper@37993: [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivative f_f'"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, neuper@37954: prls=e_rls, crls = Atools_erls, nrls = norm_diff}, neuper@37993: "Script DiffScr (f_f::real) (v_v::real) = " ^ neuper@37993: " (let f_f' = Take (d_d v_v f_f) " ^ neuper@37954: " in (( " ^ neuper@37954: " (Repeat " ^ neuper@37991: " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ neuper@37954: " (Repeat (Rewrite_Set make_polynomial False)))) " ^ neuper@37993: " )) f_f')" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_diff_equ" [] e_metID neuper@37954: (["diff","differentiate_equality"], neuper@37993: [("#Given" ,["functionEq f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivativeEq f_f'"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", rls' = erls_diff, calc = [], neuper@37954: srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff}, neuper@37993: "Script DiffEqScr (f_f::bool) (v_v::real) = " ^ neuper@37993: " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^ neuper@37991: " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ neuper@37954: " (Repeat " ^ neuper@37991: " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ neuper@37991: " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ neuper@37954: " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ neuper@37993: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_diff_after_simp" [] e_metID neuper@37954: (["diff","after_simplification"], neuper@37993: [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), neuper@37993: ("#Find" ,["derivative f_f'"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls, neuper@37954: crls=Atools_erls, nrls = norm_Rational}, neuper@37993: "Script DiffScr (f_f::real) (v_v::real) = " ^ neuper@37993: " (let f_f' = Take (d_d v_v f_f) " ^ neuper@37954: " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^ neuper@37991: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ neuper@37991: " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ neuper@37991: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ neuper@37993: " (Try (Rewrite_Set norm_Rational False))) f_f')" neuper@37954: )); neuper@37954: neuper@37954: neuper@37954: (** CAS-commands **) neuper@37954: neuper@37954: (*.handle cas-input like "Diff (a * x^3 + b, x)".*) neuper@37954: (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)"); neuper@37954: val [Const ("Pair", _) $ t $ bdv] = pairl; neuper@37954: *) neuper@37954: fun argl2dtss [Const ("Pair", _) $ t $ bdv] = neuper@37954: [((term_of o the o (parse thy)) "functionTerm", [t]), neuper@37954: ((term_of o the o (parse thy)) "differentiateFor", [bdv]), neuper@37954: ((term_of o the o (parse thy)) "derivative", neuper@37993: [(term_of o the o (parse thy)) "f_f'"]) neuper@37954: ] neuper@38031: | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; neuper@37954: castab := neuper@37954: overwritel (!castab, neuper@37954: [((term_of o the o (parse thy)) "Diff", neuper@37991: (("Isac", ["derivative_of","function"], ["no_met"]), neuper@37954: argl2dtss)) neuper@37954: ]); neuper@37954: neuper@37954: (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) neuper@37954: (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)"); neuper@37954: val [Const ("Pair", _) $ t $ bdv] = pairl; neuper@37954: *) neuper@37954: fun argl2dtss [Const ("Pair", _) $ t $ bdv] = neuper@37954: [((term_of o the o (parse thy)) "functionEq", [t]), neuper@37954: ((term_of o the o (parse thy)) "differentiateFor", [bdv]), neuper@37954: ((term_of o the o (parse thy)) "derivativeEq", neuper@37993: [(term_of o the o (parse thy)) "f_f'::bool"]) neuper@37954: ] neuper@38031: | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; neuper@37954: castab := neuper@37954: overwritel (!castab, neuper@37954: [((term_of o the o (parse thy)) "Differentiate", neuper@37991: (("Isac", ["named","derivative_of","function"], ["no_met"]), neuper@37954: argl2dtss)) neuper@37954: ]); neuper@37954: *} neuper@37954: neuper@37906: end