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

 	     ]);