(* differentiation over the reals

    author: Walther Neuper

    000516   

  *)

 theory Diff imports Calculus Trig LogExp Rational Root Poly Base_Tools begin

 ML \<open>

 @{term "sin x"}

 \<close>

 consts

   d_d           :: "[real, real]=> real"

   (*descriptions in the related problems*)

   derivativeEq  :: "bool => una"

   (*predicates*)

   primed        :: "'a => 'a" (*"primed A" -> "A'"*)

   (*the CAS-commands, eg. "Diff (2*x \<up> 3, x)", 

 			  "Differentiate (A = s * (a - s), s)"*)

   Diff           :: "[real * real] => real"

   Differentiate  :: "[bool * real] => bool"

   (*subproblem-name*)

   differentiate  :: "[char list * char list list * char list, real, real] => real"

                	   ("(differentiate (_)/ (_ _ ))" 9)

 text \<open>a variant of the derivatives defintion:

   d_d            :: "(real => real) => (real => real)"

   advantages:

 (1) no variable 'bdv' on the meta-level required

 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"

 (3) and no specialized chain-rules required like

     diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"

   disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation

 \<close>

 axiomatization where (*stated as axioms, todo: prove as theorems

         'bdv' is a constant on the meta-level  *)

   diff_const:     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" and

   diff_var:       "d_d bdv bdv = 1" and

   diff_prod_const:"[| Not (bdv occurs_in u) |] ==>  

 					 d_d bdv (u * v) = u * d_d bdv v" and

   diff_sum:       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v" and

   diff_dif:       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v" and

   diff_prod:      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v" and

   diff_quot:      "Not (v = 0) ==> (d_d bdv (u / v) =  

 	           (d_d bdv u * v - u * d_d bdv v) / v \<up> 2)" and

   diff_sin:       "d_d bdv (sin bdv)   = cos bdv" and

   diff_sin_chain: "d_d bdv (sin u)     = cos u * d_d bdv u" and

   diff_cos:       "d_d bdv (cos bdv)   = - sin bdv" and

   diff_cos_chain: "d_d bdv (cos u)     = - sin u * d_d bdv u" and

   diff_pow:       "d_d bdv (bdv \<up> n) = n * (bdv \<up> (n - 1))" and

   diff_pow_chain: "d_d bdv (u \<up> n)   = n * (u \<up> (n - 1)) * d_d bdv u" and

   diff_ln:        "d_d bdv (ln bdv)    = 1 / bdv" and

   diff_ln_chain:  "d_d bdv (ln u)      = d_d bdv u / u" and

   diff_exp:       "d_d bdv (exp bdv)   = exp bdv" and

   diff_exp_chain: "d_d bdv (exp u)     = exp u * d_d x u" and

 (*

   diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"

   diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"

 *)

   (*...*)

   frac_conv:       "[| bdv occurs_in b; 0 < n |] ==>  

 		    a / (b \<up> n) = a * b \<up> (-n)" and

   frac_sym_conv:   "n < 0 ==> a * b \<up> n = a / b \<up> (-n)" and

   sqrt_conv_bdv:   "sqrt bdv = bdv \<up> (1 / 2)" and

   sqrt_conv_bdv_n: "sqrt (bdv \<up> n) = bdv \<up> (n / 2)" and

 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)

   sqrt_conv:       "bdv occurs_in u ==> sqrt u = u \<up> (1 / 2)" and

 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)

   sqrt_sym_conv:   "u \<up> (a / 2) = sqrt (u \<up> a)" and

   root_conv:       "bdv occurs_in u ==> nroot n u = u \<up> (1 / n)" and

   root_sym_conv:   "u \<up> (a / b) = nroot b (u \<up> a)" and

   realpow_pow_bdv: "(bdv \<up> b) \<up> c = bdv \<up> (b * c)"

 ML \<open>

 val thy = @{theory};

 (** eval functions **)

 fun primed (Const (id, T)) = Const (id ^ "'", T)

   | primed (Free (id, T)) = Free (id ^ "'", T)

   | primed t = raise ERROR ("primed called with arg = '"^ UnparseC.term t ^"'");

 (*("primed", ("Diff.primed", eval_primed "#primed"))*)

 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =

     SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (primed t),

 	  HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))

   | eval_primed _ _ _ _ = NONE;

 \<close>

 setup \<open>KEStore_Elems.add_calcs

   [("primed", ("Diff.primed", eval_primed "#primed"))]\<close>

 ML \<open>

 (** rulesets **)

 (*.converts a term such that differentiation works optimally.*)

 val diff_conv =   

     Rule_Def.Repeat {id="diff_conv", 

 	 preconds = [], 

 	 rew_ord = ("termlessI",termlessI), 

 	 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty 

 			   [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),

 			    Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

 			    Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),

 			    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

 			    Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),

 			    Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false})

 			    ], 

 	 srls = Rule_Set.Empty, calc = [], errpatts = [],

 	 rules =

   [Rule.Thm ("frac_conv", ThmC.numerals_to_Free @{thm frac_conv}),

      (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"*)

 		   Rule.Thm ("sqrt_conv_bdv", ThmC.numerals_to_Free @{thm sqrt_conv_bdv}),

 		     (*"sqrt ?bdv = ?bdv \<up> (1 / 2)"*)

 		   Rule.Thm ("sqrt_conv_bdv_n", ThmC.numerals_to_Free @{thm sqrt_conv_bdv_n}),

 		     (*"sqrt (?bdv \<up> ?n) = ?bdv \<up> (?n / 2)"*)

 		   Rule.Thm ("sqrt_conv", ThmC.numerals_to_Free @{thm sqrt_conv}),

 		     (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)

 		   Rule.Thm ("root_conv", ThmC.numerals_to_Free @{thm root_conv}),

 		     (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)

 		   Rule.Thm ("realpow_pow_bdv", ThmC.numerals_to_Free @{thm realpow_pow_bdv}),

 		     (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)

 		   Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),

 		   Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),

 		     (*a / b * (c / d) = a * c / (b * d)*)

 		   Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),

 		     (*?x * (?y / ?z) = ?x * ?y / ?z*)

 		   Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left})

 		     (*?y / ?z * ?x = ?y * ?x / ?z*)

 		 ],

 	 scr = Rule.Empty_Prog};

 \<close>

 ML \<open>

 (*.beautifies a term after differentiation.*)

 val diff_sym_conv =   

     Rule_Def.Repeat {id="diff_sym_conv", 

 	 preconds = [], 

 	 rew_ord = ("termlessI",termlessI), 

 	 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty 

 		 [Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

      Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),

 	   Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),

 	   Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

 	   Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),

 	   Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})], 

 	 srls = Rule_Set.Empty, calc = [], errpatts = [],

 	 rules = 

      [Rule.Thm ("frac_sym_conv", ThmC.numerals_to_Free @{thm frac_sym_conv}),

 		 Rule.Thm ("sqrt_sym_conv", ThmC.numerals_to_Free @{thm sqrt_sym_conv}),

 		 Rule.Thm ("root_sym_conv", ThmC.numerals_to_Free @{thm root_sym_conv}),

      Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))

 	   (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),

 		 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),

 		 (*a / b * (c / d) = a * c / (b * d)*)

 		 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),

 		 (*?x * (?y / ?z) = ?x * ?y / ?z*)

 		 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),

 		 (*?y / ?z * ?x = ?y * ?x / ?z*)

 		 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_")],

 	 scr = Rule.Empty_Prog};

 (*..*)

 val srls_diff = 

     Rule_Def.Repeat {id="srls_differentiate..", 

 	 preconds = [], 

 	 rew_ord = ("termlessI",termlessI), 

 	 erls = Rule_Set.empty, 

 	 srls = Rule_Set.Empty, calc = [], errpatts = [],

 	 rules = [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),

 		  Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_"),

 		  Rule.Eval("Diff.primed", eval_primed "Diff.primed")

 		  ],

 	 scr = Rule.Empty_Prog};

 \<close>

 ML \<open>

 (*..*)

 val erls_diff = 

     Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty

                [Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

 		Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),

 		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    

 		Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),

 		Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),

 		Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")

 		];

 (*.rules for differentiation, _no_ simplification.*)

 val diff_rules =

     Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), 

 	 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],

 	 rules = [Rule.Thm ("diff_sum",ThmC.numerals_to_Free @{thm diff_sum}),

 		  Rule.Thm ("diff_dif",ThmC.numerals_to_Free @{thm diff_dif}),

 		  Rule.Thm ("diff_prod_const",ThmC.numerals_to_Free @{thm diff_prod_const}),

 		  Rule.Thm ("diff_prod",ThmC.numerals_to_Free @{thm diff_prod}),

 		  Rule.Thm ("diff_quot",ThmC.numerals_to_Free @{thm diff_quot}),

 		  Rule.Thm ("diff_sin",ThmC.numerals_to_Free @{thm diff_sin}),

 		  Rule.Thm ("diff_sin_chain",ThmC.numerals_to_Free @{thm diff_sin_chain}),

 		  Rule.Thm ("diff_cos",ThmC.numerals_to_Free @{thm diff_cos}),

 		  Rule.Thm ("diff_cos_chain",ThmC.numerals_to_Free @{thm diff_cos_chain}),

 		  Rule.Thm ("diff_pow",ThmC.numerals_to_Free @{thm diff_pow}),

 		  Rule.Thm ("diff_pow_chain",ThmC.numerals_to_Free @{thm diff_pow_chain}),

 		  Rule.Thm ("diff_ln",ThmC.numerals_to_Free @{thm diff_ln}),

 		  Rule.Thm ("diff_ln_chain",ThmC.numerals_to_Free @{thm diff_ln_chain}),

 		  Rule.Thm ("diff_exp",ThmC.numerals_to_Free @{thm diff_exp}),

 		  Rule.Thm ("diff_exp_chain",ThmC.numerals_to_Free @{thm diff_exp_chain}),

 (*

 		  Rule.Thm ("diff_sqrt",ThmC.numerals_to_Free @{thm diff_sqrt}),

 		  Rule.Thm ("diff_sqrt_chain",ThmC.numerals_to_Free @{thm diff_sqrt_chain}),

 *)

 		  Rule.Thm ("diff_const",ThmC.numerals_to_Free @{thm diff_const}),

 		  Rule.Thm ("diff_var",ThmC.numerals_to_Free @{thm diff_var})

 		  ],

 	 scr = Rule.Empty_Prog};

 \<close>

 ML \<open>

 (*.normalisation for checking user-input.*)

 val norm_diff = 

   Rule_Def.Repeat

     {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI), 

      erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

      rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],

      scr = Rule.Empty_Prog};

 \<close>

 setup \<open>KEStore_Elems.add_rlss 

   [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)), 

   ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)), 

   ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)), 

   ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)), 

   ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))]\<close>

 (** problem types **)

 setup \<open>KEStore_Elems.add_pbts

   [(Problem.prep_input thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),

     (Problem.prep_input thy "pbl_fun_deriv" [] Problem.id_empty

       (["derivative_of", "function"],

         [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),

           ("#Find"  ,["derivative f_f'"])],

         Rule_Set.append_rules "empty" Rule_Set.empty [],

         SOME "Diff (f_f, v_v)", [["diff", "differentiate_on_R"],

 			  ["diff", "after_simplification"]])),

     (*here "named" is used differently from Integration"*)

     (Problem.prep_input thy "pbl_fun_deriv_nam" [] Problem.id_empty

       (["named", "derivative_of", "function"],

         [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),

           ("#Find"  ,["derivativeEq f_f'"])],

         Rule_Set.append_rules "empty" Rule_Set.empty [],

         SOME "Differentiate (f_f, v_v)",

         [["diff", "differentiate_equality"]]))]\<close>

 ML \<open>

 (** CAS-commands **)

 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)

 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");

    val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;

    *)

 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =

     [((Thm.term_of o the o (TermC.parse thy)) "functionTerm", [t]),

      ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),

      ((Thm.term_of o the o (TermC.parse thy)) "derivative", 

       [(Thm.term_of o the o (TermC.parse thy)) "f_f'"])

      ]

   | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";

 \<close>

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_diff" [] MethodC.id_empty

       (["diff"], [],

         {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

           crls = Atools_erls, errpats = [], nrls = norm_diff},

         @{thm refl})]

 \<close>

 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"

   where

 "differentiate_on_R f_f v_v = (

   let

     f_f' = Take (d_d v_v f_f)

   in (

     (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) #> (

     Repeat (

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or

       (Repeat (Rewrite_Set ''make_polynomial'')))) #> (

     Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))

     ) f_f')"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_diff_onR" [] MethodC.id_empty

       (["diff", "differentiate_on_R"],

         [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),

           ("#Find"  ,["derivative f_f'"])],

         {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

           crls = Atools_erls, errpats = [], nrls = norm_diff},

         @{thm differentiate_on_R.simps})]

 \<close>

 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"

   where

 "differentiateX f_f v_v = (

   let

     f_f' = Take (d_d v_v f_f)

   in (

     Repeat (

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' )) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or

       (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or

       (Repeat (Rewrite_Set ''make_polynomial'')))

     ) f_f')"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_diff_simpl" [] MethodC.id_empty

       (["diff", "diff_simpl"],

         [("#Given", ["functionTerm f_f", "differentiateFor v_v"]),

          ("#Find" , ["derivative f_f'"])],

         {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

           crls = Atools_erls, errpats = [], nrls = norm_diff},

         @{thm differentiateX.simps})]

 \<close>

 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"

   where

 "differentiate_equality f_f v_v = (

   let

     f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))

   in (

     (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) #> (

     Repeat (

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif''        )) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or

       (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or

       (Repeat (Rewrite_Set ''make_polynomial'')))) #> (

     Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))

     ) f_f')"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_diff_equ" [] MethodC.id_empty

       (["diff", "differentiate_equality"],

         [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),

           ("#Find"  ,["derivativeEq f_f'"])],

         {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,

           crls=Atools_erls, errpats = [], nrls = norm_diff},

         @{thm differentiate_equality.simps})]

 \<close>

 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"

   where

 "simplify_derivative term bound_variable = (

   let

    term' = Take (d_d bound_variable term)

   in (

     (Try (Rewrite_Set ''norm_Rational'')) #>

     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) #>

     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) #>

     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) #>

     (Try (Rewrite_Set ''norm_Rational''))

     ) term')"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_diff_after_simp" [] MethodC.id_empty

       (["diff", "after_simplification"],

         [("#Given" ,["functionTerm term", "differentiateFor bound_variable"]),

           ("#Find"  ,["derivative term'"])],

         {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

           crls=Atools_erls, errpats = [], nrls = norm_Rational},

         @{thm simplify_derivative.simps})]

 \<close>

 setup \<open>KEStore_Elems.add_cas

   [((Thm.term_of o the o (TermC.parse thy)) "Diff",

 	      (("Isac_Knowledge", ["derivative_of", "function"], ["no_met"]), argl2dtss))]\<close>

 ML \<open>

 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)

 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");

    val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;

    *)

 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =

     [((Thm.term_of o the o (TermC.parse thy)) "functionEq", [t]),

      ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),

      ((Thm.term_of o the o (TermC.parse thy)) "derivativeEq", 

       [(Thm.term_of o the o (TermC.parse thy)) "f_f'::bool"])

      ]

   | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";

 \<close>

 setup \<open>KEStore_Elems.add_cas

   [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",  

 	      (("Isac_Knowledge", ["named", "derivative_of", "function"], ["no_met"]), argl2dtss))]

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end