(* tools for differentiation

   WN.11.99

use"Knowledge/Diff.ML";

use"Diff.ML";

 *)

(** interface isabelle -- isac **)

theory' := overwritel (!theory', [("Diff.thy",Diff.thy)]);

(** 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 = '"^ term2str t ^"'");

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

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

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

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

  | eval_primed _ _ _ _ = NONE;

calclist':= overwritel (!calclist', 

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

    ]);

(** 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",num_str not_true),

			    Thm ("not_false",num_str not_false),

			    Calc ("op <",eval_equ "#less_"),

			    Thm ("and_true",num_str and_true),

			    Thm ("and_false",num_str and_false)

			    ], 

	 srls = Erls, calc = [],

	 rules = [Thm ("frac_conv", num_str frac_conv),

		  Thm ("sqrt_conv_bdv", num_str sqrt_conv_bdv),

		  Thm ("sqrt_conv_bdv_n", num_str sqrt_conv_bdv_n),

		  Thm ("sqrt_conv", num_str sqrt_conv),

		  Thm ("root_conv", num_str root_conv),

		  Thm ("realpow_pow_bdv", num_str realpow_pow_bdv),

		  Calc ("op *", eval_binop "#mult_"),

		  Thm ("rat_mult",num_str rat_mult),

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

		  Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),

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

		  Thm ("real_times_divide2_eq",num_str real_times_divide2_eq)

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

		  (*

		  Thm ("", num_str ),*)

		 ],

	 scr = EmptyScr};

(*.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 ("op <",eval_equ "#less_")

			    ], 

	 srls = Erls, calc = [],

	 rules = [Thm ("frac_sym_conv", num_str frac_sym_conv),

		  Thm ("sqrt_sym_conv", num_str sqrt_sym_conv),

		  Thm ("root_sym_conv", num_str root_sym_conv),

		  Thm ("sym_real_mult_minus1",

		       num_str (real_mult_minus1 RS sym)),

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

		  Thm ("rat_mult",num_str rat_mult),

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

		  Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),

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

		  Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),

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

		  Calc ("op *", eval_binop "#mult_")

		 ],

	 scr = EmptyScr};

(*..*)

val srls_diff = 

    Rls {id="srls_differentiate..", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = e_rls, 

	 srls = Erls, calc = [],

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

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

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

		  ],

	 scr = EmptyScr};

(*..*)

val erls_diff = 

    append_rls "erls_differentiate.." e_rls

               [Thm ("not_true",num_str not_true),

		Thm ("not_false",num_str 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 = [],

	 rules = [Thm ("diff_sum",num_str diff_sum),

		  Thm ("diff_dif",num_str diff_dif),

		  Thm ("diff_prod_const",num_str diff_prod_const),

		  Thm ("diff_prod",num_str diff_prod),

		  Thm ("diff_quot",num_str diff_quot),

		  Thm ("diff_sin",num_str diff_sin),

		  Thm ("diff_sin_chain",num_str diff_sin_chain),

		  Thm ("diff_cos",num_str diff_cos),

		  Thm ("diff_cos_chain",num_str diff_cos_chain),

		  Thm ("diff_pow",num_str diff_pow),

		  Thm ("diff_pow_chain",num_str diff_pow_chain),

		  Thm ("diff_ln",num_str diff_ln),

		  Thm ("diff_ln_chain",num_str diff_ln_chain),

		  Thm ("diff_exp",num_str diff_exp),

		  Thm ("diff_exp_chain",num_str diff_exp_chain),

(*

		  Thm ("diff_sqrt",num_str diff_sqrt),

		  Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),

*)

		  Thm ("diff_const",num_str diff_const),

		  Thm ("diff_var",num_str diff_var)

		  ],

	 scr = EmptyScr};

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

val norm_diff = 

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

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

	 rules = [Rls_ diff_rules,

		  Rls_ norm_Poly

		  ],

	 scr = EmptyScr};

ruleset' := 

overwritelthy thy (!ruleset', 

	    [("diff_rules", prep_rls norm_diff),

	     ("norm_diff", prep_rls norm_diff),

	     ("diff_conv", prep_rls diff_conv),

	     ("diff_sym_conv", prep_rls diff_sym_conv)

	     ]);

(** problem types **)

store_pbt

 (prep_pbt Diff.thy "pbl_fun" [] e_pblID

 (["function"], [], e_rls, NONE, []));

store_pbt

 (prep_pbt Diff.thy "pbl_fun_deriv" [] e_pblID

 (["derivative_of","function"],

  [("#Given" ,["functionTerm f_","differentiateFor v_"]),

   ("#Find"  ,["derivative f_'_"])

  ],

  append_rls "e_rls" e_rls [],

  SOME "Diff (f_, v_)", [["diff","differentiate_on_R"],

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

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

store_pbt

 (prep_pbt Diff.thy "pbl_fun_deriv_nam" [] e_pblID

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

  [("#Given" ,["functionEq f_","differentiateFor v_"]),

   ("#Find"  ,["derivativeEq f_'_"])

  ],

  append_rls "e_rls" e_rls [],

  SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));

(** methods **)

store_met

 (prep_met Diff.thy "met_diff" [] e_metID

 (["diff"], [],

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

    crls = Atools_erls, nrls = norm_diff}, "empty_script"));

store_met

 (prep_met Diff.thy "met_diff_onR" [] e_metID

 (["diff","differentiate_on_R"],

   [("#Given" ,["functionTerm f_","differentiateFor v_"]),

    ("#Find"  ,["derivative f_'_"])

    ],

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

    prls=e_rls, crls = Atools_erls, nrls = norm_diff},

"Script DiffScr (f_::real) (v_::real) =                          \

\ (let f'_ = Take (d_d v_ f_)                                    \

\ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@    \

\ (Repeat                                                        \

\   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or \

\    (Repeat (Rewrite_Set             make_polynomial False)))) @@ \

\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"

));

store_met

 (prep_met Diff.thy "met_diff_simpl" [] e_metID

 (["diff","diff_simpl"],

   [("#Given" ,["functionTerm f_","differentiateFor v_"]),

    ("#Find"  ,["derivative f_'_"])

    ],

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

    prls=e_rls, crls = Atools_erls, nrls = norm_diff},

"Script DiffScr (f_::real) (v_::real) =                          \

\ (let f'_ = Take (d_d v_ f_)                                    \

\ in ((     \

\ (Repeat                                                        \

\   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or \

\    (Repeat (Rewrite_Set             make_polynomial False))))  \

\ )) f'_)"

 ));

(*-----------------------------------------------------------------

 "Script DiffScr (f_::real) (v_::real) =                \

 \(Repeat                                           \

 \   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or \

 \    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or \

 \    (Repeat (Rewrite_Set             make_polynomial False)))) \

 \ (f_::real)"

*)

store_met

 (prep_met Diff.thy "met_diff_equ" [] e_metID

 (["diff","differentiate_equality"],

   [("#Given" ,["functionEq f_","differentiateFor v_"]),

   ("#Find"  ,["derivativeEq f_'_"])

  ],

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

    srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},

"Script DiffEqScr (f_::bool) (v_::real) =                          \

\ (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_))            \

\ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@      \

\ (Repeat                                                          \

\   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or   \

\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or   \

\    (Repeat (Rewrite_Set             make_polynomial False)))) @@ \

\ (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"

));

store_met

 (prep_met Diff.thy "met_diff_after_simp" [] e_metID

 (["diff","after_simplification"],

   [("#Given" ,["functionTerm f_","differentiateFor v_"]),

    ("#Find"  ,["derivative f_'_"])

    ],

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

    crls=Atools_erls, nrls = norm_Rational},

"Script DiffScr (f_::real) (v_::real) =                          \

\ (let f'_ = Take (d_d v_ f_)                                    \

\ in ((Try (Rewrite_Set norm_Rational False)) @@                 \

\     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@     \

\     (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@     \

\     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ \

\     (Try (Rewrite_Set norm_Rational False))) f'_)"

));

(** 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 ("Pair", _) $ t $ bdv] = pairl;

   *)

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

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

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

     ((term_of o the o (parse thy)) "derivative", 

      [(term_of o the o (parse thy)) "f_'_"])

     ]

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

castab := 

overwritel (!castab, 

	    [((term_of o the o (parse thy)) "Diff",  

	      (("Isac.thy", ["derivative_of","function"], ["no_met"]), 

	       argl2dtss))

	     ]);

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

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

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

   *)

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

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

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

     ((term_of o the o (parse thy)) "derivativeEq", 

      [(term_of o the o (parse thy)) "f_'_::bool"])

     ]

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

castab := 

overwritel (!castab, 

	    [((term_of o the o (parse thy)) "Differentiate",  

	      (("Isac.thy", ["named","derivative_of","function"], ["no_met"]), 

	       argl2dtss))

	     ]);