(* differentiation over the reals

   author: Walther Neuper

   000516   

 *)

theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin

ML {*

@{term "sin x"}

*}

consts

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

(*sin, cos      :: "real => real"      already in Isabelle2009-2*)

(*

  log, ln       :: "real => real"

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

  exp           :: "real => real"         ("E'_ ^^^ _" 80)

*)

  (*descriptions in the related problems*)

  derivativeEq  :: "bool => una"

  (*predicates*)

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

  (*the CAS-commands, eg. "Diff (2*x^^^3, x)", 

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

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

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

  (*subproblem and script-name*)

  differentiate  :: "[ID * (ID list) * ID, real,real] => real"

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

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

                   ("((Script DiffScr (_ _ =))// (_))" 9)

  DiffEqScr      :: "[bool,real,  bool] => bool"

                   ("((Script DiffEqScr (_ _ =))// (_))" 9)

text {*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

*}

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 ^^^ 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 ^^^ n) = n * (bdv ^^^ (n - 1))" and

  diff_pow_chain: "d_d bdv (u ^^^ n)   = n * (u ^^^ (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 ^^^ n) = a * b ^^^ (-n)" and

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

  sqrt_conv_bdv:   "sqrt bdv = bdv ^^^ (1 / 2)" and

  sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" and

  sqrt_conv:       "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" and

  sqrt_sym_conv:   "u ^^^ (a / 2) = sqrt (u ^^^ a)" and

  root_conv:       "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" and

  root_sym_conv:   "u ^^^ (a / b) = nroot b (u ^^^ a)" and

  realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"

ML {*

val thy = @{theory};

(** eval functions **)

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

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

  | primed t = error ("primed called with arg = '"^ term2str t ^"'");

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

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

    SOME ((term2str p) ^ " = " ^ term2str (primed t),

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

  | eval_primed _ _ _ _ = NONE;

*}

setup {* KEStore_Elems.add_calcs

  [("primed", ("Diff.primed", eval_primed "#primed"))] *}

ML {*

(** rulesets **)

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

val diff_conv =   

    Rls {id="diff_conv", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = append_rls "erls_diff_conv" e_rls 

			   [Calc ("Atools.occurs'_in", eval_occurs_in ""),

			    Thm ("not_true",TermC.num_str @{thm not_true}),

			    Thm ("not_false",TermC.num_str @{thm not_false}),

			    Calc ("Orderings.ord_class.less",eval_equ "#less_"),

			    Thm ("and_true",TermC.num_str @{thm and_true}),

			    Thm ("and_false",TermC.num_str @{thm and_false})

			    ], 

	 srls = Erls, calc = [], errpatts = [],

	 rules =

  [Thm ("frac_conv", TermC.num_str @{thm frac_conv}),

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

		   Thm ("sqrt_conv_bdv", TermC.num_str @{thm sqrt_conv_bdv}),

		     (*"sqrt ?bdv = ?bdv ^^^ (1 / 2)"*)

		   Thm ("sqrt_conv_bdv_n", TermC.num_str @{thm sqrt_conv_bdv_n}),

		     (*"sqrt (?bdv ^^^ ?n) = ?bdv ^^^ (?n / 2)"*)

		   Thm ("sqrt_conv", TermC.num_str @{thm sqrt_conv}),

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

		   Thm ("root_conv", TermC.num_str @{thm root_conv}),

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

		   Thm ("realpow_pow_bdv", TermC.num_str @{thm realpow_pow_bdv}),

		     (* "(?bdv ^^^ ?b) ^^^ ?c = ?bdv ^^^ (?b * ?c)"*)

		   Calc ("Groups.times_class.times", eval_binop "#mult_"),

		   Thm ("rat_mult",TermC.num_str @{thm rat_mult}),

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

		   Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),

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

		   Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left})

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

		 ],

	 scr = EmptyScr};

*}

ML {*

(*.beautifies a term after differentiation.*)

val diff_sym_conv =   

    Rls {id="diff_sym_conv", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = append_rls "erls_diff_sym_conv" e_rls 

			   [Calc ("Orderings.ord_class.less",eval_equ "#less_")

			    ], 

	 srls = Erls, calc = [], errpatts = [],

	 rules = [Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),

		  Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),

		  Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),

		  Thm ("sym_real_mult_minus1",

		       TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),

		      (*- ?z = "-1 * ?z"*)

		  Thm ("rat_mult",TermC.num_str @{thm rat_mult}),

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

		  Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),

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

		  Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),

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

		  Calc ("Groups.times_class.times", eval_binop "#mult_")

		 ],

	 scr = EmptyScr};

(*..*)

val srls_diff = 

    Rls {id="srls_differentiate..", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = e_rls, 

	 srls = Erls, calc = [], errpatts = [],

	 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),

		  Calc("Tools.rhs", eval_rhs "eval_rhs_"),

		  Calc("Diff.primed", eval_primed "Diff.primed")

		  ],

	 scr = EmptyScr};

*}

ML {*

(*..*)

val erls_diff = 

    append_rls "erls_differentiate.." e_rls

               [Thm ("not_true",TermC.num_str @{thm not_true}),

		Thm ("not_false",TermC.num_str @{thm not_false}),

		Calc ("Atools.ident",eval_ident "#ident_"),    

		Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),

		Calc ("Atools.occurs'_in",eval_occurs_in ""),

		Calc ("Atools.is'_const",eval_const "#is_const_")

		];

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

val diff_rules =

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

	 erls = erls_diff, srls = Erls, calc = [], errpatts = [],

	 rules = [Thm ("diff_sum",TermC.num_str @{thm diff_sum}),

		  Thm ("diff_dif",TermC.num_str @{thm diff_dif}),

		  Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),

		  Thm ("diff_prod",TermC.num_str @{thm diff_prod}),

		  Thm ("diff_quot",TermC.num_str @{thm diff_quot}),

		  Thm ("diff_sin",TermC.num_str @{thm diff_sin}),

		  Thm ("diff_sin_chain",TermC.num_str @{thm diff_sin_chain}),

		  Thm ("diff_cos",TermC.num_str @{thm diff_cos}),

		  Thm ("diff_cos_chain",TermC.num_str @{thm diff_cos_chain}),

		  Thm ("diff_pow",TermC.num_str @{thm diff_pow}),

		  Thm ("diff_pow_chain",TermC.num_str @{thm diff_pow_chain}),

		  Thm ("diff_ln",TermC.num_str @{thm diff_ln}),

		  Thm ("diff_ln_chain",TermC.num_str @{thm diff_ln_chain}),

		  Thm ("diff_exp",TermC.num_str @{thm diff_exp}),

		  Thm ("diff_exp_chain",TermC.num_str @{thm diff_exp_chain}),

(*

		  Thm ("diff_sqrt",TermC.num_str @{thm diff_sqrt}),

		  Thm ("diff_sqrt_chain",TermC.num_str @{thm diff_sqrt_chain}),

*)

		  Thm ("diff_const",TermC.num_str @{thm diff_const}),

		  Thm ("diff_var",TermC.num_str @{thm diff_var})

		  ],

	 scr = EmptyScr};

*}

ML {*

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

val norm_diff = 

  Rls

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

     erls = Erls, srls = Erls, calc = [], errpatts = [],

     rules = [Rls_ diff_rules, Rls_ norm_Poly ],

     scr = EmptyScr};

*}

setup {* 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))] *}

(** problem types **)

setup {* KEStore_Elems.add_pbts

  [(Specify.prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),

    (Specify.prep_pbt thy "pbl_fun_deriv" [] e_pblID

      (["derivative_of","function"],

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

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

        append_rls "e_rls" e_rls [],

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

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

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

    (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID

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

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

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

        append_rls "e_rls" e_rls [],

        SOME "Differentiate (f_f, v_v)",

        [["diff","differentiate_equality"]]))] *}

ML {*

(** 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 _ = error "Diff.ML: wrong argument for argl2dtss";

*}

setup {* KEStore_Elems.add_mets

  [Specify.prep_met thy "met_diff" [] e_metID

      (["diff"], [],

        {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

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

        "empty_script"),

    Specify.prep_met thy "met_diff_onR" [] e_metID

      (["diff","differentiate_on_R"],

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

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

        {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,

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

        "Script DiffScr (f_f::real) (v_v::real) =                          " ^

          " (let f_f' = Take (d_d v_v f_f)                                    " ^

          " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@    " ^

          " (Repeat                                                        " ^

          "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^

          "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^

          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),

    Specify.prep_met thy "met_diff_simpl" [] e_metID

      (["diff","diff_simpl"],

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

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

        {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,

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

        "Script DiffScr (f_f::real) (v_v::real) =                           " ^

          " (let f_f' = Take (d_d v_v f_f)                                  " ^

          " in ((                                                           " ^

          " (Repeat                                                         " ^

          "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^

          "    (Repeat (Rewrite_Set              make_polynomial False))))  " ^

          " )) f_f')"),

    Specify.prep_met thy "met_diff_equ" [] e_metID

      (["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=e_rls,

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

        "Script DiffEqScr (f_f::bool) (v_v::real) =                          " ^

          " (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 False)) @@      " ^

          " (Repeat                                                          " ^

          "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or   " ^

          "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or   " ^

          "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^

          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),

    Specify.prep_met thy "met_diff_after_simp" [] e_metID

      (["diff","after_simplification"],

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

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

        {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,

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

        "Script DiffScr (f_f::real) (v_v::real) =                          " ^

          " (let f_f' = Take (d_d v_v f_f)                                    " ^

          " in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^

          "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@     " ^

          "     (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@     " ^

          "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^

          "     (Try (Rewrite_Set norm_Rational False))) f_f')")]

*}

setup {* KEStore_Elems.add_cas

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

	      (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *}

ML {*

(*.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 _ = error "Diff.ML: wrong argument for argl2dtss";

*}

setup {* KEStore_Elems.add_cas

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

	      (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *}

end