Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Diff.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37983 03bfbc480107
child 37993 e4796b1125fb
permissions -rw-r--r--
tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \; 
     1 (* differentiation over the reals

     2    author: Walther Neuper

     3    000516   

     4  *)

     5 

     6 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin

     7 

     8 consts

     9 

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

    11   sin, cos      :: "real => real"

    12 (*

    13   log, ln       :: "real => real"

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

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

    16 *)

    17   (*descriptions in the related problems*)

    18   derivativeEq  :: bool => una

    19 

    20   (*predicates*)

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

    22 

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

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

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

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

    27 

    28   (*subproblem and script-name*)

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

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

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

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

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

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

    35 

    36 text {*a variant of the derivatives defintion:

    37 

    38   d_d            :: "(real => real) => (real => real)"

    39 

    40   advantages:

    41 (1) no variable 'bdv' on the meta-level required

    42 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"

    43 (3) and no specialized chain-rules required like

    44     diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"

    45 

    46   disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation

    47 *}

    48 

    49 axioms (*stated as axioms, todo: prove as theorems

    50         'bdv' is a constant on the meta-level  *)

    51   diff_const:     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"

    52   diff_var:       "d_d bdv bdv = 1"

    53   diff_prod_const:"[| Not (bdv occurs_in u) |] ==>  

    54 					 d_d bdv (u * v) = u * d_d bdv v"

    55 

    56   diff_sum:       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v"

    57   diff_dif:       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v"

    58   diff_prod:      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v"

    59   diff_quot:      "Not (v = 0) ==> (d_d bdv (u / v) =  

    60 	           (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"

    61 

    62   diff_sin:       "d_d bdv (sin bdv)   = cos bdv"

    63   diff_sin_chain: "d_d bdv (sin u)     = cos u * d_d bdv u"

    64   diff_cos:       "d_d bdv (cos bdv)   = - sin bdv"

    65   diff_cos_chain: "d_d bdv (cos u)     = - sin u * d_d bdv u"

    66   diff_pow:       "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"

    67   diff_pow_chain: "d_d bdv (u ^^^ n)   = n * (u ^^^ (n - 1)) * d_d bdv u"

    68   diff_ln:        "d_d bdv (ln bdv)    = 1 / bdv"

    69   diff_ln_chain:  "d_d bdv (ln u)      = d_d bdv u / u"

    70   diff_exp:       "d_d bdv (exp bdv)   = exp bdv"

    71   diff_exp_chain: "d_d bdv (exp u)     = exp u * d_d x u"

    72 (*

    73   diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"

    74   diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"

    75 *)

    76   (*...*)

    77 

    78   frac_conv:       "[| bdv occurs_in b; 0 < n |] ==>  

    79 		    a / (b ^^^ n) = a * b ^^^ (-n)"

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

    81 

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

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

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

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

    86 

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

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

    89 

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

    91 

    92 ML {*

    93 val thy = @{theory};

    94 

    95 (** eval functions **)

    96 

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

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

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

   100 

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

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

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

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

   105   | eval_primed _ _ _ _ = NONE;

   106 

   107 calclist':= overwritel (!calclist', 

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

   109     ]);

   110 

   111 

   112 (** rulesets **)

   113 

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

   115 val diff_conv =   

   116     Rls {id="diff_conv", 

   117 	 preconds = [], 

   118 	 rew_ord = ("termlessI",termlessI), 

   119 	 erls = append_rls "erls_diff_conv" e_rls 

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

   121 			    Thm ("not_true",num_str @{thm not_true}),

   122 			    Thm ("not_false",num_str @{thm not_false}),

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

   124 			    Thm ("and_true",num_str @{thm and_true}),

   125 			    Thm ("and_false",num_str @{thm and_false)

   126 			    ], 

   127 	 srls = Erls, calc = [],

   128 	 rules = [Thm ("frac_conv", num_str @{thm frac_conv}),

   129 		  Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}),

   130 		  Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}),

   131 		  Thm ("sqrt_conv", num_str @{thm sqrt_conv}),

   132 		  Thm ("root_conv", num_str @{thm root_conv}),

   133 		  Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}),

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

   135 		  Thm ("rat_mult",num_str @{thm rat_mult}),

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

   137 		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),

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

   139 		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})

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

   141 		  (*

   142 		  Thm ("", num_str @{}),*)

   143 		 ],

   144 	 scr = EmptyScr};

   145 

   146 (*.beautifies a term after differentiation.*)

   147 val diff_sym_conv =   

   148     Rls {id="diff_sym_conv", 

   149 	 preconds = [], 

   150 	 rew_ord = ("termlessI",termlessI), 

   151 	 erls = append_rls "erls_diff_sym_conv" e_rls 

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

   153 			    ], 

   154 	 srls = Erls, calc = [],

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

   156 		  Thm ("sqrt_sym_conv", num_str @{thm sqrt_sym_conv}),

   157 		  Thm ("root_sym_conv", num_str @{thm root_sym_conv}),

   158 		  Thm ("sym_real_mult_minus1",

   159 		       num_str (@{thm real_mult_minus1} RS @{thm sym})),

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

   161 		  Thm ("rat_mult",num_str @{thm rat_mult}),

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

   163 		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),

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

   165 		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),

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

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

   168 		 ],

   169 	 scr = EmptyScr};

   170 

   171 (*..*)

   172 val srls_diff = 

   173     Rls {id="srls_differentiate..", 

   174 	 preconds = [], 

   175 	 rew_ord = ("termlessI",termlessI), 

   176 	 erls = e_rls, 

   177 	 srls = Erls, calc = [],

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

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

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

   181 		  ],

   182 	 scr = EmptyScr};

   183 

   184 (*..*)

   185 val erls_diff = 

   186     append_rls "erls_differentiate.." e_rls

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

   188 		Thm ("not_false",num_str @{thm not_false}),

   189 		

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

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

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

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

   194 		];

   195 

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

   197 val diff_rules =

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

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

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

   201 		  Thm ("diff_dif",num_str @{thm diff_dif}),

   202 		  Thm ("diff_prod_const",num_str @{thm diff_prod_const}),

   203 		  Thm ("diff_prod",num_str @{thm diff_prod}),

   204 		  Thm ("diff_quot",num_str @{thm diff_quot}),

   205 		  Thm ("diff_sin",num_str @{thm diff_sin}),

   206 		  Thm ("diff_sin_chain",num_str @{thm diff_sin_chain}),

   207 		  Thm ("diff_cos",num_str @{thm diff_cos}),

   208 		  Thm ("diff_cos_chain",num_str @{thm diff_cos_chain}),

   209 		  Thm ("diff_pow",num_str @{thm diff_pow}),

   210 		  Thm ("diff_pow_chain",num_str @{thm diff_pow_chain}),

   211 		  Thm ("diff_ln",num_str @{thm diff_ln}),

   212 		  Thm ("diff_ln_chain",num_str @{thm diff_ln_chain}),

   213 		  Thm ("diff_exp",num_str @{thm diff_exp}),

   214 		  Thm ("diff_exp_chain",num_str @{thm diff_exp_chain}),

   215 (*

   216 		  Thm ("diff_sqrt",num_str @{thm diff_sqrt}),

   217 		  Thm ("diff_sqrt_chain",num_str @{thm diff_sqrt_chain}),

   218 *)

   219 		  Thm ("diff_const",num_str @{thm diff_const}),

   220 		  Thm ("diff_var",num_str @{thm diff_var})

   221 		  ],

   222 	 scr = EmptyScr};

   223 

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

   225 val norm_diff = 

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

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

   228 	 rules = [Rls_ diff_rules,

   229 		  Rls_ norm_Poly

   230 		  ],

   231 	 scr = EmptyScr};

   232 ruleset' := 

   233 overwritelthy @{theory} (!ruleset', 

   234 	    [("diff_rules", prep_rls norm_diff),

   235 	     ("norm_diff", prep_rls norm_diff),

   236 	     ("diff_conv", prep_rls diff_conv),

   237 	     ("diff_sym_conv", prep_rls diff_sym_conv)

   238 	     ]);

   239 

   240 

   241 (** problem types **)

   242 

   243 store_pbt

   244  (prep_pbt thy "pbl_fun" [] e_pblID

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

   246 

   247 store_pbt

   248  (prep_pbt thy "pbl_fun_deriv" [] e_pblID

   249  (["derivative_of","function"],

   250   [("#Given" ,["functionTerm f_","differentiateFor v_v"]),

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

   252   ],

   253   append_rls "e_rls" e_rls [],

   254   SOME "Diff (f_, v_v)", [["diff","differentiate_on_R"],

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

   256 

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

   258 store_pbt

   259  (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID

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

   261   [("#Given" ,["functionEq f_","differentiateFor v_v"]),

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

   263   ],

   264   append_rls "e_rls" e_rls [],

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

   266 

   267 

   268 (** methods **)

   269 

   270 store_met

   271  (prep_met thy "met_diff" [] e_metID

   272  (["diff"], [],

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

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

   275 

   276 store_met

   277  (prep_met thy "met_diff_onR" [] e_metID

   278  (["diff","differentiate_on_R"],

   279    [("#Given" ,["functionTerm f_","differentiateFor v_v"]),

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

   281     ],

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

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

   284 "Script DiffScr (f_::real) (v_v::real) =                          " ^

   285 " (let f'_ = Take (d_d v_v f_)                                    " ^

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

   287 " (Repeat                                                        " ^

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   305 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"

   306 ));

   307 

   308 store_met

   309  (prep_met thy "met_diff_simpl" [] e_metID

   310  (["diff","diff_simpl"],

   311    [("#Given" ,["functionTerm f_","differentiateFor v_v"]),

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

   313     ],

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

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

   316 "Script DiffScr (f_::real) (v_v::real) =                          " ^

   317 " (let f'_ = Take (d_d v_v f_)                                    " ^

   318 " in ((     " ^

   319 " (Repeat                                                        " ^

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   337 " )) f'_)"

   338  ));

   339     

   340 store_met

   341  (prep_met thy "met_diff_equ" [] e_metID

   342  (["diff","differentiate_equality"],

   343    [("#Given" ,["functionEq f_","differentiateFor v_v"]),

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

   345   ],

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

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

   348 "Script DiffEqScr (f_::bool) (v_v::real) =                          " ^

   349 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_))            " ^

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

   351 " (Repeat                                                          " ^

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   370 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"

   371 ));

   372 

   373 store_met

   374  (prep_met thy "met_diff_after_simp" [] e_metID

   375  (["diff","after_simplification"],

   376    [("#Given" ,["functionTerm f_","differentiateFor v_v"]),

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

   378     ],

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

   380     crls=Atools_erls, nrls = norm_Rational},

   381 "Script DiffScr (f_::real) (v_v::real) =                          " ^

   382 " (let f'_ = Take (d_d v_v f_)                                    " ^

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

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

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

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

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

   388 ));

   389 

   390 

   391 (** CAS-commands **)

   392 

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

   394 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");

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

   396    *)

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

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

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

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

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

   402      ]

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

   404 castab := 

   405 overwritel (!castab, 

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

   407 	      (("Isac", ["derivative_of","function"], ["no_met"]), 

   408 	       argl2dtss))

   409 	     ]);

   410 

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

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

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

   414    *)

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

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

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

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

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

   420      ]

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

   422 castab := 

   423 overwritel (!castab, 

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

   425 	      (("Isac", ["named","derivative_of","function"], ["no_met"]), 

   426 	       argl2dtss))

   427 	     ]);

   428 *}

   429 

   430 end
wneuper/isa