
neuper@37906: (* differentiation over the reals
neuper@37906:    author: Walther Neuper
neuper@37906:    000516   
neuper@37906:  *)
neuper@37906: 
neuper@37954: theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
neuper@37906: 
neuper@37993: ML {*
neuper@37993: @{term "sin x"}
neuper@37993: *}
neuper@37993: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   d_d           :: "[real, real]=> real"
neuper@37993: (*sin, cos      :: "real => real"      already in Isabelle2009-2*)
neuper@37906: (*
neuper@37906:   log, ln       :: "real => real"
neuper@37906:   nlog          :: "[real, real] => real"
neuper@37906:   exp           :: "real => real"         ("E'_ ^^^ _" 80)
neuper@37906: *)
neuper@37906:   (*descriptions in the related problems*)
neuper@37993:   derivativeEq  :: "bool => una"
neuper@37906: 
neuper@37906:   (*predicates*)
neuper@37906:   primed        :: "'a => 'a" (*"primed A" -> "A'"*)
neuper@37906: 
neuper@37906:   (*the CAS-commands, eg. "Diff (2*x^^^3, x)", 
neuper@37906: 			  "Differentiate (A = s * (a - s), s)"*)
neuper@37906:   Diff           :: "[real * real] => real"
neuper@37906:   Differentiate  :: "[bool * real] => bool"
neuper@37906: 
neuper@37906:   (*subproblem and script-name*)
neuper@37906:   differentiate  :: "[ID * (ID list) * ID, real,real] => real"
neuper@37906:                	   ("(differentiate (_)/ (_ _ ))" 9)
neuper@37906:   DiffScr        :: "[real,real,  real] => real"
neuper@37906:                    ("((Script DiffScr (_ _ =))// (_))" 9)
neuper@37993:   DiffEqScr      :: "[bool,real,  bool] => bool"
neuper@37906:                    ("((Script DiffEqScr (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37954: text {*a variant of the derivatives defintion:
neuper@37906: 
neuper@37954:   d_d            :: "(real => real) => (real => real)"
neuper@37954: 
neuper@37954:   advantages:
neuper@37954: (1) no variable 'bdv' on the meta-level required
neuper@37954: (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
neuper@37954: (3) and no specialized chain-rules required like
neuper@37954:     diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"
neuper@37954: 
neuper@37954:   disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
neuper@37954: *}
neuper@37954: 
neuper@37954: axioms (*stated as axioms, todo: prove as theorems
neuper@37906:         'bdv' is a constant on the meta-level  *)
neuper@37983:   diff_const:     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
neuper@37983:   diff_var:       "d_d bdv bdv = 1"
neuper@37983:   diff_prod_const:"[| Not (bdv occurs_in u) |] ==>  
neuper@37954: 					 d_d bdv (u * v) = u * d_d bdv v"
neuper@37906: 
neuper@37983:   diff_sum:       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v"
neuper@37983:   diff_dif:       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v"
neuper@37983:   diff_prod:      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v"
neuper@37983:   diff_quot:      "Not (v = 0) ==> (d_d bdv (u / v) =  
neuper@37954: 	           (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
neuper@37906: 
neuper@37983:   diff_sin:       "d_d bdv (sin bdv)   = cos bdv"
neuper@37983:   diff_sin_chain: "d_d bdv (sin u)     = cos u * d_d bdv u"
neuper@37983:   diff_cos:       "d_d bdv (cos bdv)   = - sin bdv"
neuper@37983:   diff_cos_chain: "d_d bdv (cos u)     = - sin u * d_d bdv u"
neuper@37983:   diff_pow:       "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
neuper@37983:   diff_pow_chain: "d_d bdv (u ^^^ n)   = n * (u ^^^ (n - 1)) * d_d bdv u"
neuper@37983:   diff_ln:        "d_d bdv (ln bdv)    = 1 / bdv"
neuper@37983:   diff_ln_chain:  "d_d bdv (ln u)      = d_d bdv u / u"
neuper@37983:   diff_exp:       "d_d bdv (exp bdv)   = exp bdv"
neuper@37983:   diff_exp_chain: "d_d bdv (exp u)     = exp u * d_d x u"
neuper@37906: (*
neuper@37906:   diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"
neuper@37906:   diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"
neuper@37906: *)
neuper@37906:   (*...*)
neuper@37906: 
neuper@37983:   frac_conv:       "[| bdv occurs_in b; 0 < n |] ==>  
neuper@37954: 		    a / (b ^^^ n) = a * b ^^^ (-n)"
neuper@37983:   frac_sym_conv:   "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
neuper@37906: 
neuper@37983:   sqrt_conv_bdv:   "sqrt bdv = bdv ^^^ (1 / 2)"
neuper@37983:   sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
neuper@37983:   sqrt_conv:       "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
neuper@37983:   sqrt_sym_conv:   "u ^^^ (a / 2) = sqrt (u ^^^ a)"
neuper@37906: 
neuper@37983:   root_conv:       "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
neuper@37983:   root_sym_conv:   "u ^^^ (a / b) = nroot b (u ^^^ a)"
neuper@37906: 
neuper@37983:   realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
neuper@37906: 
neuper@37954: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37954: (** eval functions **)
neuper@37954: 
neuper@37954: fun primed (Const (id, T)) = Const (id ^ "'", T)
neuper@37954:   | primed (Free (id, T)) = Free (id ^ "'", T)
neuper@38031:   | primed t = error ("primed called with arg = '"^ term2str t ^"'");
neuper@37954: 
neuper@37954: (*("primed", ("Diff.primed", eval_primed "#primed"))*)
neuper@37954: fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
neuper@37954:     SOME ((term2str p) ^ " = " ^ term2str (primed t),
neuper@37954: 	  Trueprop $ (mk_equality (p, primed t)))
neuper@37954:   | eval_primed _ _ _ _ = NONE;
neuper@37954: 
neuper@37954: calclist':= overwritel (!calclist', 
neuper@37954:    [("primed", ("Diff.primed", eval_primed "#primed"))
neuper@37954:     ]);
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: (** rulesets **)
neuper@37954: 
neuper@37954: (*.converts a term such that differentiation works optimally.*)
neuper@37954: val diff_conv =   
neuper@37954:     Rls {id="diff_conv", 
neuper@37954: 	 preconds = [], 
neuper@37954: 	 rew_ord = ("termlessI",termlessI), 
neuper@37954: 	 erls = append_rls "erls_diff_conv" e_rls 
neuper@37954: 			   [Calc ("Atools.occurs'_in", eval_occurs_in ""),
neuper@37969: 			    Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 			    Thm ("not_false",num_str @{thm not_false}),
neuper@37954: 			    Calc ("op <",eval_equ "#less_"),
neuper@37969: 			    Thm ("and_true",num_str @{thm and_true}),
neuper@37993: 			    Thm ("and_false",num_str @{thm and_false})
neuper@37954: 			    ], 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37969: 	 rules = [Thm ("frac_conv", num_str @{thm frac_conv}),
neuper@37969: 		  Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}),
neuper@37969: 		  Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}),
neuper@37969: 		  Thm ("sqrt_conv", num_str @{thm sqrt_conv}),
neuper@37969: 		  Thm ("root_conv", num_str @{thm root_conv}),
neuper@37969: 		  Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}),
neuper@37954: 		  Calc ("op *", eval_binop "#mult_"),
neuper@37969: 		  Thm ("rat_mult",num_str @{thm rat_mult}),
neuper@37954: 		  (*a / b * (c / d) = a * c / (b * d)*)
neuper@37965: 		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
neuper@37954: 		  (*?x * (?y / ?z) = ?x * ?y / ?z*)
neuper@37965: 		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
neuper@37954: 		  (*?y / ?z * ?x = ?y * ?x / ?z*)
neuper@37954: 		 ],
neuper@37954: 	 scr = EmptyScr};
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: (*.beautifies a term after differentiation.*)
neuper@37954: val diff_sym_conv =   
neuper@37954:     Rls {id="diff_sym_conv", 
neuper@37954: 	 preconds = [], 
neuper@37954: 	 rew_ord = ("termlessI",termlessI), 
neuper@37954: 	 erls = append_rls "erls_diff_sym_conv" e_rls 
neuper@37954: 			   [Calc ("op <",eval_equ "#less_")
neuper@37954: 			    ], 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37969: 	 rules = [Thm ("frac_sym_conv", num_str @{thm frac_sym_conv}),
neuper@37969: 		  Thm ("sqrt_sym_conv", num_str @{thm sqrt_sym_conv}),
neuper@37969: 		  Thm ("root_sym_conv", num_str @{thm root_sym_conv}),
neuper@37954: 		  Thm ("sym_real_mult_minus1",
neuper@37969: 		       num_str (@{thm real_mult_minus1} RS @{thm sym})),
neuper@37954: 		      (*- ?z = "-1 * ?z"*)
neuper@37969: 		  Thm ("rat_mult",num_str @{thm rat_mult}),
neuper@37954: 		  (*a / b * (c / d) = a * c / (b * d)*)
neuper@37965: 		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
neuper@37954: 		  (*?x * (?y / ?z) = ?x * ?y / ?z*)
neuper@37965: 		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
neuper@37954: 		  (*?y / ?z * ?x = ?y * ?x / ?z*)
neuper@37954: 		  Calc ("op *", eval_binop "#mult_")
neuper@37954: 		 ],
neuper@37954: 	 scr = EmptyScr};
neuper@37954: 
neuper@37954: (*..*)
neuper@37954: val srls_diff = 
neuper@37954:     Rls {id="srls_differentiate..", 
neuper@37954: 	 preconds = [], 
neuper@37954: 	 rew_ord = ("termlessI",termlessI), 
neuper@37954: 	 erls = e_rls, 
neuper@37954: 	 srls = Erls, calc = [],
neuper@37954: 	 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
neuper@37954: 		  Calc("Tools.rhs", eval_rhs "eval_rhs_"),
neuper@37954: 		  Calc("Diff.primed", eval_primed "Diff.primed")
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: (*..*)
neuper@37954: val erls_diff = 
neuper@37954:     append_rls "erls_differentiate.." e_rls
neuper@37969:                [Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 		Thm ("not_false",num_str @{thm not_false}),
neuper@37954: 		
neuper@37954: 		Calc ("Atools.ident",eval_ident "#ident_"),    
neuper@37954: 		Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
neuper@37954: 		Calc ("Atools.occurs'_in",eval_occurs_in ""),
neuper@37954: 		Calc ("Atools.is'_const",eval_const "#is_const_")
neuper@37954: 		];
neuper@37954: 
neuper@37954: (*.rules for differentiation, _no_ simplification.*)
neuper@37954: val diff_rules =
neuper@37954:     Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37954: 	 erls = erls_diff, srls = Erls, calc = [],
neuper@37969: 	 rules = [Thm ("diff_sum",num_str @{thm diff_sum}),
neuper@37969: 		  Thm ("diff_dif",num_str @{thm diff_dif}),
neuper@37969: 		  Thm ("diff_prod_const",num_str @{thm diff_prod_const}),
neuper@37969: 		  Thm ("diff_prod",num_str @{thm diff_prod}),
neuper@37969: 		  Thm ("diff_quot",num_str @{thm diff_quot}),
neuper@37969: 		  Thm ("diff_sin",num_str @{thm diff_sin}),
neuper@37969: 		  Thm ("diff_sin_chain",num_str @{thm diff_sin_chain}),
neuper@37969: 		  Thm ("diff_cos",num_str @{thm diff_cos}),
neuper@37969: 		  Thm ("diff_cos_chain",num_str @{thm diff_cos_chain}),
neuper@37969: 		  Thm ("diff_pow",num_str @{thm diff_pow}),
neuper@37969: 		  Thm ("diff_pow_chain",num_str @{thm diff_pow_chain}),
neuper@37969: 		  Thm ("diff_ln",num_str @{thm diff_ln}),
neuper@37969: 		  Thm ("diff_ln_chain",num_str @{thm diff_ln_chain}),
neuper@37969: 		  Thm ("diff_exp",num_str @{thm diff_exp}),
neuper@37969: 		  Thm ("diff_exp_chain",num_str @{thm diff_exp_chain}),
neuper@37954: (*
neuper@37969: 		  Thm ("diff_sqrt",num_str @{thm diff_sqrt}),
neuper@37969: 		  Thm ("diff_sqrt_chain",num_str @{thm diff_sqrt_chain}),
neuper@37954: *)
neuper@37969: 		  Thm ("diff_const",num_str @{thm diff_const}),
neuper@37969: 		  Thm ("diff_var",num_str @{thm diff_var})
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: (*.normalisation for checking user-input.*)
neuper@37954: val norm_diff = 
neuper@37954:     Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37954: 	 erls = Erls, srls = Erls, calc = [],
neuper@37954: 	 rules = [Rls_ diff_rules,
neuper@37954: 		  Rls_ norm_Poly
neuper@37954: 		  ],
neuper@37954: 	 scr = EmptyScr};
neuper@37954: ruleset' := 
neuper@37967: overwritelthy @{theory} (!ruleset', 
neuper@37954: 	    [("diff_rules", prep_rls norm_diff),
neuper@37954: 	     ("norm_diff", prep_rls norm_diff),
neuper@37954: 	     ("diff_conv", prep_rls diff_conv),
neuper@37954: 	     ("diff_sym_conv", prep_rls diff_sym_conv)
neuper@37954: 	     ]);
neuper@37954: 
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: (** problem types **)
neuper@37954: 
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_fun" [] e_pblID
neuper@37954:  (["function"], [], e_rls, NONE, []));
neuper@37954: 
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_fun_deriv" [] e_pblID
neuper@37954:  (["derivative_of","function"],
neuper@37993:   [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
neuper@37993:    ("#Find"  ,["derivative f_f'"])
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [],
neuper@37993:   SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
neuper@37954: 			 ["diff","after_simplification"]]));
neuper@37954: 
neuper@37954: (*here "named" is used differently from Integration"*)
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
neuper@37954:  (["named","derivative_of","function"],
neuper@37993:   [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
neuper@37993:    ("#Find"  ,["derivativeEq f_f'"])
neuper@37954:   ],
neuper@37954:   append_rls "e_rls" e_rls [],
neuper@37993:   SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: 
neuper@37954: (** methods **)
neuper@37954: 
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_diff" [] e_metID
neuper@37954:  (["diff"], [],
neuper@37954:    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37954:     crls = Atools_erls, nrls = norm_diff}, "empty_script"));
neuper@37954: 
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_diff_onR" [] e_metID
neuper@37954:  (["diff","differentiate_on_R"],
neuper@37993:    [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
neuper@37993:     ("#Find"  ,["derivative f_f'"])
neuper@37954:     ],
neuper@37954:    {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, 
neuper@37954:     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
neuper@37993: "Script DiffScr (f_f::real) (v_v::real) =                          " ^
neuper@37993: " (let f_f' = Take (d_d v_v f_f)                                    " ^
neuper@37991: " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@    " ^
neuper@37954: " (Repeat                                                        " ^
neuper@37991: "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
neuper@37954: "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
neuper@37993: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
neuper@37954: ));
neuper@37993: *}
neuper@37993: ML {*
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_diff_simpl" [] e_metID
neuper@37954:  (["diff","diff_simpl"],
neuper@37993:    [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
neuper@37993:     ("#Find"  ,["derivative f_f'"])
neuper@37954:     ],
neuper@37954:    {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
neuper@37954:     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
neuper@37993: "Script DiffScr (f_f::real) (v_v::real) =                          " ^
neuper@37993: " (let f_f' = Take (d_d v_v f_f)                                    " ^
neuper@37954: " in ((     " ^
neuper@37954: " (Repeat                                                        " ^
neuper@37991: "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
neuper@37954: "    (Repeat (Rewrite_Set             make_polynomial False))))  " ^
neuper@37993: " )) f_f')"
neuper@37954:  ));
neuper@37954:     
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_diff_equ" [] e_metID
neuper@37954:  (["diff","differentiate_equality"],
neuper@37993:    [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
neuper@37993:    ("#Find"  ,["derivativeEq f_f'"])
neuper@37954:   ],
neuper@37954:    {rew_ord'="tless_true", rls' = erls_diff, calc = [], 
neuper@37954:     srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
neuper@37993: "Script DiffEqScr (f_f::bool) (v_v::real) =                          " ^
neuper@37993: " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))            " ^
neuper@37991: " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@      " ^
neuper@37954: " (Repeat                                                          " ^
neuper@37991: "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or   " ^
neuper@37991: "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or   " ^
neuper@37954: "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
neuper@37993: " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
neuper@37954: ));
neuper@37954: 
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_diff_after_simp" [] e_metID
neuper@37954:  (["diff","after_simplification"],
neuper@37993:    [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
neuper@37993:     ("#Find"  ,["derivative f_f'"])
neuper@37954:     ],
neuper@37954:    {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
neuper@37954:     crls=Atools_erls, nrls = norm_Rational},
neuper@37993: "Script DiffScr (f_f::real) (v_v::real) =                          " ^
neuper@37993: " (let f_f' = Take (d_d v_v f_f)                                    " ^
neuper@37954: " in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^
neuper@37991: "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@     " ^
neuper@37991: "     (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@     " ^
neuper@37991: "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
neuper@37993: "     (Try (Rewrite_Set norm_Rational False))) f_f')"
neuper@37954: ));
neuper@37954: 
neuper@37954: 
neuper@37954: (** CAS-commands **)
neuper@37954: 
neuper@37954: (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
neuper@37954: (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
neuper@37954:    val [Const ("Pair", _) $ t $ bdv] = pairl;
neuper@37954:    *)
neuper@37954: fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
neuper@37954:     [((term_of o the o (parse thy)) "functionTerm", [t]),
neuper@37954:      ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
neuper@37954:      ((term_of o the o (parse thy)) "derivative", 
neuper@37993:       [(term_of o the o (parse thy)) "f_f'"])
neuper@37954:      ]
neuper@38031:   | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
neuper@37954: castab := 
neuper@37954: overwritel (!castab, 
neuper@37954: 	    [((term_of o the o (parse thy)) "Diff",  
neuper@37991: 	      (("Isac", ["derivative_of","function"], ["no_met"]), 
neuper@37954: 	       argl2dtss))
neuper@37954: 	     ]);
neuper@37954: 
neuper@37954: (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
neuper@37954: (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
neuper@37954:    val [Const ("Pair", _) $ t $ bdv] = pairl;
neuper@37954:    *)
neuper@37954: fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
neuper@37954:     [((term_of o the o (parse thy)) "functionEq", [t]),
neuper@37954:      ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
neuper@37954:      ((term_of o the o (parse thy)) "derivativeEq", 
neuper@37993:       [(term_of o the o (parse thy)) "f_f'::bool"])
neuper@37954:      ]
neuper@38031:   | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
neuper@37954: castab := 
neuper@37954: overwritel (!castab, 
neuper@37954: 	    [((term_of o the o (parse thy)) "Differentiate",  
neuper@37991: 	      (("Isac", ["named","derivative_of","function"], ["no_met"]), 
neuper@37954: 	       argl2dtss))
neuper@37954: 	     ]);
neuper@37954: *}
neuper@37954: 
neuper@37906: end




