(* 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>

(** 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 @{context} t ^"'");

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

fun eval_primed _ _ (p as (Const (\<^const_name>\<open>Diff.primed\<close>,_) $ t)) _ =

    SOME ((UnparseC.term @{context} p) ^ " = " ^ UnparseC.term @{context} (primed t),

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

  | eval_primed _ _ _ _ = NONE;

\<close>

calculation primed = \<open>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), 

  asm_rls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty [

    \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),

    \<^rule_thm>\<open>not_true\<close>,

    \<^rule_thm>\<open>not_false\<close>,

    \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

    \<^rule_thm>\<open>and_true\<close>,

    \<^rule_thm>\<open>and_false\<close>], 

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

  rules = [

     \<^rule_thm>\<open>frac_conv\<close>, (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"*)

 	   \<^rule_thm>\<open>sqrt_conv_bdv\<close>, (*"sqrt ?bdv = ?bdv \<up> (1 / 2)"*)

 	   \<^rule_thm>\<open>sqrt_conv_bdv_n\<close>, (*"sqrt (?bdv \<up> ?n) = ?bdv \<up> (?n / 2)"*)

 	   \<^rule_thm>\<open>sqrt_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)

 	   \<^rule_thm>\<open>root_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)

 	   \<^rule_thm>\<open>realpow_pow_bdv\<close>, (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)

 	   \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),

 	   \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)

 	   \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)

 	   \<^rule_thm>\<open>times_divide_eq_left\<close>], (*?y / ?z * ?x = ?y * ?x / ?z*)

  program = 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), 

  asm_rls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty [

    \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), 

    \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),

    \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),

    \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),

    \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

    \<^rule_thm>\<open>not_false\<close>,

    \<^rule_thm>\<open>not_true\<close>], 

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

  rules = [

    \<^rule_thm>\<open>frac_sym_conv\<close>,

    \<^rule_thm>\<open>sqrt_sym_conv\<close>,

    \<^rule_thm>\<open>root_sym_conv\<close>,

    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_atom) ==> - (z::real) = -1 * z"*),

    \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?a) = ?a"*),

    \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),

    \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),

    \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),

    \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_")],

  program = Rule.Empty_Prog};

(*..*)

val srls_diff = 

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

  asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

  rules = [

    \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),

    \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_"),

    \<^rule_eval>\<open>Diff.primed\<close> (eval_primed "Diff.primed")],

  program = Rule.Empty_Prog};

\<close>

ML \<open>

(*..*)

val erls_diff = 

  Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty [

    \<^rule_thm>\<open>not_true\<close>,

		\<^rule_thm>\<open>not_false\<close>,

		\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),

		\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),

		\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),

  	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];

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

val diff_rules =

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

	 asm_rls = erls_diff, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

	 rules = [

      \<^rule_thm>\<open>diff_sum\<close>,

		  \<^rule_thm>\<open>diff_dif\<close>,

		  \<^rule_thm>\<open>diff_prod_const\<close>,

		  \<^rule_thm>\<open>diff_prod\<close>,

		  \<^rule_thm>\<open>diff_quot\<close>,

		  \<^rule_thm>\<open>diff_sin\<close>,

		  \<^rule_thm>\<open>diff_sin_chain\<close>,

		  \<^rule_thm>\<open>diff_cos\<close>,

		  \<^rule_thm>\<open>diff_cos_chain\<close>,

		  \<^rule_thm>\<open>diff_pow\<close>,

		  \<^rule_thm>\<open>diff_pow_chain\<close>,

		  \<^rule_thm>\<open>diff_ln\<close>,

		  \<^rule_thm>\<open>diff_ln_chain\<close>,

		  \<^rule_thm>\<open>diff_exp\<close>,

		  \<^rule_thm>\<open>diff_exp_chain\<close>,

      (*

		  \<^rule_thm>\<open>diff_sqrt\<close>,

		  \<^rule_thm>\<open>diff_sqrt_chain\<close>,

      *)

		  \<^rule_thm>\<open>diff_const\<close>,

		  \<^rule_thm>\<open>diff_var\<close>],

	 program = 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), 

     asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

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

     program = Rule.Empty_Prog};

\<close>

rule_set_knowledge

  erls_diff = \<open>prep_rls' erls_diff\<close> and

  diff_rules = \<open>prep_rls' diff_rules\<close> and

  norm_diff = \<open>prep_rls' norm_diff\<close> and

  diff_conv = \<open>prep_rls' diff_conv\<close> and

  diff_sym_conv = \<open>prep_rls' diff_sym_conv\<close>

(** problems **)

problem pbl_fun : "function" = \<open>Rule_Set.empty\<close>

problem pbl_fun_deriv : "derivative_of/function" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method_Ref: "diff/differentiate_on_R" "diff/after_simplification"

  CAS: "Diff (f_f, v_v)"

  Given: "functionTerm f_f" "differentiateFor v_v"

  Find: "derivative f_f'"

problem pbl_fun_deriv_nam :

  "named/derivative_of/function" (*here "named" is used differently from Integration"*) =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method_Ref: "diff/differentiate_equality"

  CAS: "Differentiate (f_f, v_v)"

  Given: "functionEq f_f" "differentiateFor v_v"

  Find: "derivativeEq f_f'"

ML \<open>

(** CAS-commands **)

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

(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)");

   val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;

   *)

fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =

    [(Syntax.read_term (Proof_Context.init_global \<^theory>) "functionTerm", [t]),

     (Syntax.read_term (Proof_Context.init_global \<^theory>) "differentiateFor", [bdv]),

     (Syntax.read_term (Proof_Context.init_global \<^theory>) "derivative", 

       [Syntax.read_term (Proof_Context.init_global \<^theory>) "f_f'"])]

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

\<close>

method met_diff : "diff" =

  \<open>{rew_ord="tless_true",rls'=Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = norm_diff}\<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')"

method met_diff_onR : "diff/differentiate_on_R" =

  \<open>{rew_ord="tless_true", rls' = erls_diff, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = norm_diff}\<close>

  Program: differentiate_on_R.simps

  Given: "functionTerm f_f" "differentiateFor v_v"

  Find: "derivative f_f'"

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')"

method met_diff_simpl : "diff/diff_simpl" =

  \<open>{rew_ord="tless_true", rls' = erls_diff, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = norm_diff}\<close>

  Program: differentiateX.simps

  Given: "functionTerm f_f" " differentiateFor v_v"

  Find: "derivative f_f'"

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')"

method met_diff_equ : "diff/differentiate_equality" =

  \<open>{rew_ord="tless_true", rls' = erls_diff, calc = [], prog_rls = srls_diff, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = norm_diff}\<close>

  Program: differentiate_equality.simps

  Given: "functionEq f_f" "differentiateFor v_v"

  Find: "derivativeEq f_f'"

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')"

method met_diff_after_simp : "diff/after_simplification" =

  \<open>{rew_ord="tless_true", rls' = Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = norm_Rational}\<close>

  Program: simplify_derivative.simps

  Given: "functionTerm term" "differentiateFor bound_variable"

  Find: "derivative term'"

cas Diff = \<open>argl2dtss\<close>

  Problem_Ref: "derivative_of/function"

ML \<open>

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

(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)");

   val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;

   *)

fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =

    [(Syntax.read_term (Proof_Context.init_global \<^theory>) "functionEq", [t]),

     (Syntax.read_term (Proof_Context.init_global \<^theory>) "differentiateFor", [bdv]),

     (Syntax.read_term (Proof_Context.init_global \<^theory>) "derivativeEq", 

       [Syntax.read_term (Proof_Context.init_global \<^theory>) "f_f'::bool"])]

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

\<close>

cas Differentiate = \<open>argl2dtss\<close>

  Problem_Ref: "named/derivative_of/function"

section \<open>Error_Patterns\<close>

declare [[check_unique = false]]

setup \<open>Know_Store.add_mets @{context}

  [Pbl_Met_Hierarchy.add_errpats @{theory} ["diff", "differentiate_on_R"]

    [("chain-rule-diff-both",

      [ParseC.patt_opt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)" |> the,

       ParseC.patt_opt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)" |> the,

       ParseC.patt_opt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)" |> the(*,

       ParseC.patt_opt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u" |> the,

       ParseC.patt_opt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u" |> the*)],

      [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}(*, @{thm diff_ln_chain},

        @{thm  diff_exp_chain}*)])]

  ]\<close>

declare [[check_unique = true]]

(*WN230105 ? do fill_ins really work wrt. substitutions ?*)

setup \<open>Error_Pattern.store_fill_ins

  [("diff_sin_chain",

    ([("fill-d_d-arg",

      ParseC.patt_opt @{theory} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _" |> the, "chain-rule-diff-both"),

    ("fill-both-args",

      ParseC.patt_opt @{theory} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _" |> the, "chain-rule-diff-both"),

    ("fill-d_d",

      ParseC.patt_opt @{theory} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u" |> the, "chain-rule-diff-both"),

    ("fill-inner-deriv",

      ParseC.patt_opt @{theory} "d_d ?bdv (sin ?u) = cos ?u * _" |> the, "chain-rule-diff-both"),

    ("fill-all",

      ParseC.patt_opt @{theory} "d_d ?bdv (sin ?u) = _" |> the, "chain-rule-diff-both")])),

  ("diff_cos_chain",

    ([("fill-d_d-arg",

      ParseC.patt_opt @{theory} "d_d ?bdv (cos ?u) = cos ?u * d_d ?bdv _" |> the, "chain-rule-diff-both"),

    ("fill-both-args",

      ParseC.patt_opt @{theory} "d_d ?bdv (cos _) = cos ?u * d_d ?bdv _" |> the, "chain-rule-diff-both"),

    ("fill-d_d",

      ParseC.patt_opt @{theory} "d_d ?bdv (cos ?u) = cos ?u * _ ?bdv ?u" |> the, "chain-rule-diff-both"),

    ("fill-inner-deriv",

      ParseC.patt_opt @{theory} "d_d ?bdv (cos ?u) = cos ?u * _" |> the, "chain-rule-diff-both"),

    ("fill-all",

      ParseC.patt_opt @{theory} "d_d ?bdv (cos ?u) = _" |> the, "chain-rule-diff-both")])),

  ("diff_pow_chain",

    ([("fill-d_d-arg",

      ParseC.patt_opt @{theory} "d_d ?bdv (?u \<up> ?n) = _" |> the, "chain-rule-diff-both")]))

  ]

\<close>

(** )

ML \<open>

    val fill_ins = get_fill_ins @{theory Diff} "chain-rule-diff-both"

ERROR: (*Unfinished theory "Diff"\<^here>*)

+ see success at end of Isac_Knowledge.thy 

\<close>

( **)

(* still ununsed; planned for stepToErrorpattern: this is just a reminder... 

insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]

  (["chain-rule-diff-both", "cancel"]: errpatID list);

[[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]

  since Know_Store.set_ref_last_thy has been shifted below;

  this ERROR will vanish during re-engineering towards Know_Store.]]]

   ...and all other related rls by hand;

   TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY

*)

ML \<open>

\<close> ML \<open>

\<close>

end