src/Tools/isac/Knowledge/Diff.thy
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 31 Aug 2010 16:00:13 +0200
branchisac-update-Isa09-2
changeset 37966 78938fc8e022
parent 37965 9c11005c33b8
child 37967 bd4f7a35e892
permissions -rw-r--r--
num_str --> num_str @{thm
neuper@37906
     1
(* differentiation over the reals
neuper@37906
     2
   author: Walther Neuper
neuper@37906
     3
   000516   
neuper@37906
     4
 *)
neuper@37906
     5
neuper@37954
     6
theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
neuper@37906
     7
neuper@37906
     8
consts
neuper@37906
     9
neuper@37906
    10
  d_d           :: "[real, real]=> real"
neuper@37906
    11
  sin, cos      :: "real => real"
neuper@37906
    12
(*
neuper@37906
    13
  log, ln       :: "real => real"
neuper@37906
    14
  nlog          :: "[real, real] => real"
neuper@37906
    15
  exp           :: "real => real"         ("E'_ ^^^ _" 80)
neuper@37906
    16
*)
neuper@37906
    17
  (*descriptions in the related problems*)
neuper@37906
    18
  derivativeEq  :: bool => una
neuper@37906
    19
neuper@37906
    20
  (*predicates*)
neuper@37906
    21
  primed        :: "'a => 'a" (*"primed A" -> "A'"*)
neuper@37906
    22
neuper@37906
    23
  (*the CAS-commands, eg. "Diff (2*x^^^3, x)", 
neuper@37906
    24
			  "Differentiate (A = s * (a - s), s)"*)
neuper@37906
    25
  Diff           :: "[real * real] => real"
neuper@37906
    26
  Differentiate  :: "[bool * real] => bool"
neuper@37906
    27
neuper@37906
    28
  (*subproblem and script-name*)
neuper@37906
    29
  differentiate  :: "[ID * (ID list) * ID, real,real] => real"
neuper@37906
    30
               	   ("(differentiate (_)/ (_ _ ))" 9)
neuper@37906
    31
  DiffScr        :: "[real,real,  real] => real"
neuper@37906
    32
                   ("((Script DiffScr (_ _ =))// (_))" 9)
neuper@37906
    33
  DiffEqScr   :: "[bool,real,  bool] => bool"
neuper@37906
    34
                   ("((Script DiffEqScr (_ _ =))// (_))" 9)
neuper@37906
    35
neuper@37954
    36
text {*a variant of the derivatives defintion:
neuper@37906
    37
neuper@37954
    38
  d_d            :: "(real => real) => (real => real)"
neuper@37954
    39
neuper@37954
    40
  advantages:
neuper@37954
    41
(1) no variable 'bdv' on the meta-level required
neuper@37954
    42
(2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
neuper@37954
    43
(3) and no specialized chain-rules required like
neuper@37954
    44
    diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"
neuper@37954
    45
neuper@37954
    46
  disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
neuper@37954
    47
*}
neuper@37954
    48
neuper@37954
    49
axioms (*stated as axioms, todo: prove as theorems
neuper@37906
    50
        'bdv' is a constant on the meta-level  *)
neuper@37906
    51
  diff_const     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
neuper@37906
    52
  diff_var       "d_d bdv bdv = 1"
neuper@37954
    53
  diff_prod_const"[| Not (bdv occurs_in u) |] ==>  
neuper@37954
    54
					 d_d bdv (u * v) = u * d_d bdv v"
neuper@37906
    55
neuper@37906
    56
  diff_sum       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v"
neuper@37906
    57
  diff_dif       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v"
neuper@37906
    58
  diff_prod      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v"
neuper@37954
    59
  diff_quot      "Not (v = 0) ==> (d_d bdv (u / v) =  
neuper@37954
    60
	           (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
neuper@37906
    61
neuper@37906
    62
  diff_sin       "d_d bdv (sin bdv)   = cos bdv"
neuper@37906
    63
  diff_sin_chain "d_d bdv (sin u)     = cos u * d_d bdv u"
neuper@37906
    64
  diff_cos       "d_d bdv (cos bdv)   = - sin bdv"
neuper@37906
    65
  diff_cos_chain "d_d bdv (cos u)     = - sin u * d_d bdv u"
neuper@37906
    66
  diff_pow       "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
neuper@37906
    67
  diff_pow_chain "d_d bdv (u ^^^ n)   = n * (u ^^^ (n - 1)) * d_d bdv u"
neuper@37906
    68
  diff_ln        "d_d bdv (ln bdv)    = 1 / bdv"
neuper@37906
    69
  diff_ln_chain  "d_d bdv (ln u)      = d_d bdv u / u"
neuper@37906
    70
  diff_exp       "d_d bdv (exp bdv)   = exp bdv"
neuper@37906
    71
  diff_exp_chain "d_d bdv (exp u)     = exp u * d_d x u"
neuper@37906
    72
(*
neuper@37906
    73
  diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"
neuper@37906
    74
  diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"
neuper@37906
    75
*)
neuper@37906
    76
  (*...*)
neuper@37906
    77
neuper@37954
    78
  frac_conv       "[| bdv occurs_in b; 0 < n |] ==>  
neuper@37954
    79
		    a / (b ^^^ n) = a * b ^^^ (-n)"
neuper@37906
    80
  frac_sym_conv   "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
neuper@37906
    81
neuper@37906
    82
  sqrt_conv_bdv   "sqrt bdv = bdv ^^^ (1 / 2)"
neuper@37906
    83
  sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
neuper@37906
    84
  sqrt_conv       "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
neuper@37906
    85
  sqrt_sym_conv   "u ^^^ (a / 2) = sqrt (u ^^^ a)"
neuper@37906
    86
neuper@37906
    87
  root_conv       "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
neuper@37906
    88
  root_sym_conv   "u ^^^ (a / b) = nroot b (u ^^^ a)"
neuper@37906
    89
neuper@37906
    90
  realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
neuper@37906
    91
neuper@37954
    92
ML {*
neuper@37954
    93
(** eval functions **)
neuper@37954
    94
neuper@37954
    95
fun primed (Const (id, T)) = Const (id ^ "'", T)
neuper@37954
    96
  | primed (Free (id, T)) = Free (id ^ "'", T)
neuper@37954
    97
  | primed t = raise error ("primed called with arg = '"^ term2str t ^"'");
neuper@37954
    98
neuper@37954
    99
(*("primed", ("Diff.primed", eval_primed "#primed"))*)
neuper@37954
   100
fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
neuper@37954
   101
    SOME ((term2str p) ^ " = " ^ term2str (primed t),
neuper@37954
   102
	  Trueprop $ (mk_equality (p, primed t)))
neuper@37954
   103
  | eval_primed _ _ _ _ = NONE;
neuper@37954
   104
neuper@37954
   105
calclist':= overwritel (!calclist', 
neuper@37954
   106
   [("primed", ("Diff.primed", eval_primed "#primed"))
neuper@37954
   107
    ]);
neuper@37954
   108
neuper@37954
   109
neuper@37954
   110
(** rulesets **)
neuper@37954
   111
neuper@37954
   112
(*.converts a term such that differentiation works optimally.*)
neuper@37954
   113
val diff_conv =   
neuper@37954
   114
    Rls {id="diff_conv", 
neuper@37954
   115
	 preconds = [], 
neuper@37954
   116
	 rew_ord = ("termlessI",termlessI), 
neuper@37954
   117
	 erls = append_rls "erls_diff_conv" e_rls 
neuper@37954
   118
			   [Calc ("Atools.occurs'_in", eval_occurs_in ""),
neuper@37966
   119
			    Thm ("not_true",num_str @{not_true),
neuper@37966
   120
			    Thm ("not_false",num_str @{not_false),
neuper@37954
   121
			    Calc ("op <",eval_equ "#less_"),
neuper@37966
   122
			    Thm ("and_true",num_str @{and_true),
neuper@37966
   123
			    Thm ("and_false",num_str @{and_false)
neuper@37954
   124
			    ], 
neuper@37954
   125
	 srls = Erls, calc = [],
neuper@37966
   126
	 rules = [Thm ("frac_conv", num_str @{frac_conv),
neuper@37966
   127
		  Thm ("sqrt_conv_bdv", num_str @{sqrt_conv_bdv),
neuper@37966
   128
		  Thm ("sqrt_conv_bdv_n", num_str @{sqrt_conv_bdv_n),
neuper@37966
   129
		  Thm ("sqrt_conv", num_str @{sqrt_conv),
neuper@37966
   130
		  Thm ("root_conv", num_str @{root_conv),
neuper@37966
   131
		  Thm ("realpow_pow_bdv", num_str @{realpow_pow_bdv),
neuper@37954
   132
		  Calc ("op *", eval_binop "#mult_"),
neuper@37966
   133
		  Thm ("rat_mult",num_str @{rat_mult),
neuper@37954
   134
		  (*a / b * (c / d) = a * c / (b * d)*)
neuper@37965
   135
		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
neuper@37954
   136
		  (*?x * (?y / ?z) = ?x * ?y / ?z*)
neuper@37965
   137
		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
neuper@37954
   138
		  (*?y / ?z * ?x = ?y * ?x / ?z*)
neuper@37954
   139
		  (*
neuper@37966
   140
		  Thm ("", num_str @{),*)
neuper@37954
   141
		 ],
neuper@37954
   142
	 scr = EmptyScr};
neuper@37954
   143
neuper@37954
   144
(*.beautifies a term after differentiation.*)
neuper@37954
   145
val diff_sym_conv =   
neuper@37954
   146
    Rls {id="diff_sym_conv", 
neuper@37954
   147
	 preconds = [], 
neuper@37954
   148
	 rew_ord = ("termlessI",termlessI), 
neuper@37954
   149
	 erls = append_rls "erls_diff_sym_conv" e_rls 
neuper@37954
   150
			   [Calc ("op <",eval_equ "#less_")
neuper@37954
   151
			    ], 
neuper@37954
   152
	 srls = Erls, calc = [],
neuper@37966
   153
	 rules = [Thm ("frac_sym_conv", num_str @{frac_sym_conv),
neuper@37966
   154
		  Thm ("sqrt_sym_conv", num_str @{sqrt_sym_conv),
neuper@37966
   155
		  Thm ("root_sym_conv", num_str @{root_sym_conv),
neuper@37954
   156
		  Thm ("sym_real_mult_minus1",
neuper@37966
   157
		       num_str @{(real_mult_minus1 RS sym)),
neuper@37954
   158
		      (*- ?z = "-1 * ?z"*)
neuper@37966
   159
		  Thm ("rat_mult",num_str @{rat_mult),
neuper@37954
   160
		  (*a / b * (c / d) = a * c / (b * d)*)
neuper@37965
   161
		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
neuper@37954
   162
		  (*?x * (?y / ?z) = ?x * ?y / ?z*)
neuper@37965
   163
		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
neuper@37954
   164
		  (*?y / ?z * ?x = ?y * ?x / ?z*)
neuper@37954
   165
		  Calc ("op *", eval_binop "#mult_")
neuper@37954
   166
		 ],
neuper@37954
   167
	 scr = EmptyScr};
neuper@37954
   168
neuper@37954
   169
(*..*)
neuper@37954
   170
val srls_diff = 
neuper@37954
   171
    Rls {id="srls_differentiate..", 
neuper@37954
   172
	 preconds = [], 
neuper@37954
   173
	 rew_ord = ("termlessI",termlessI), 
neuper@37954
   174
	 erls = e_rls, 
neuper@37954
   175
	 srls = Erls, calc = [],
neuper@37954
   176
	 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
neuper@37954
   177
		  Calc("Tools.rhs", eval_rhs "eval_rhs_"),
neuper@37954
   178
		  Calc("Diff.primed", eval_primed "Diff.primed")
neuper@37954
   179
		  ],
neuper@37954
   180
	 scr = EmptyScr};
neuper@37954
   181
neuper@37954
   182
(*..*)
neuper@37954
   183
val erls_diff = 
neuper@37954
   184
    append_rls "erls_differentiate.." e_rls
neuper@37966
   185
               [Thm ("not_true",num_str @{not_true),
neuper@37966
   186
		Thm ("not_false",num_str @{not_false),
neuper@37954
   187
		
neuper@37954
   188
		Calc ("Atools.ident",eval_ident "#ident_"),    
neuper@37954
   189
		Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
neuper@37954
   190
		Calc ("Atools.occurs'_in",eval_occurs_in ""),
neuper@37954
   191
		Calc ("Atools.is'_const",eval_const "#is_const_")
neuper@37954
   192
		];
neuper@37954
   193
neuper@37954
   194
(*.rules for differentiation, _no_ simplification.*)
neuper@37954
   195
val diff_rules =
neuper@37954
   196
    Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37954
   197
	 erls = erls_diff, srls = Erls, calc = [],
neuper@37966
   198
	 rules = [Thm ("diff_sum",num_str @{diff_sum),
neuper@37966
   199
		  Thm ("diff_dif",num_str @{diff_dif),
neuper@37966
   200
		  Thm ("diff_prod_const",num_str @{diff_prod_const),
neuper@37966
   201
		  Thm ("diff_prod",num_str @{diff_prod),
neuper@37966
   202
		  Thm ("diff_quot",num_str @{diff_quot),
neuper@37966
   203
		  Thm ("diff_sin",num_str @{diff_sin),
neuper@37966
   204
		  Thm ("diff_sin_chain",num_str @{diff_sin_chain),
neuper@37966
   205
		  Thm ("diff_cos",num_str @{diff_cos),
neuper@37966
   206
		  Thm ("diff_cos_chain",num_str @{diff_cos_chain),
neuper@37966
   207
		  Thm ("diff_pow",num_str @{diff_pow),
neuper@37966
   208
		  Thm ("diff_pow_chain",num_str @{diff_pow_chain),
neuper@37966
   209
		  Thm ("diff_ln",num_str @{diff_ln),
neuper@37966
   210
		  Thm ("diff_ln_chain",num_str @{diff_ln_chain),
neuper@37966
   211
		  Thm ("diff_exp",num_str @{diff_exp),
neuper@37966
   212
		  Thm ("diff_exp_chain",num_str @{diff_exp_chain),
neuper@37954
   213
(*
neuper@37966
   214
		  Thm ("diff_sqrt",num_str @{diff_sqrt),
neuper@37966
   215
		  Thm ("diff_sqrt_chain",num_str @{diff_sqrt_chain),
neuper@37954
   216
*)
neuper@37966
   217
		  Thm ("diff_const",num_str @{diff_const),
neuper@37966
   218
		  Thm ("diff_var",num_str @{diff_var)
neuper@37954
   219
		  ],
neuper@37954
   220
	 scr = EmptyScr};
neuper@37954
   221
neuper@37954
   222
(*.normalisation for checking user-input.*)
neuper@37954
   223
val norm_diff = 
neuper@37954
   224
    Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37954
   225
	 erls = Erls, srls = Erls, calc = [],
neuper@37954
   226
	 rules = [Rls_ diff_rules,
neuper@37954
   227
		  Rls_ norm_Poly
neuper@37954
   228
		  ],
neuper@37954
   229
	 scr = EmptyScr};
neuper@37954
   230
ruleset' := 
neuper@37954
   231
overwritelthy thy (!ruleset', 
neuper@37954
   232
	    [("diff_rules", prep_rls norm_diff),
neuper@37954
   233
	     ("norm_diff", prep_rls norm_diff),
neuper@37954
   234
	     ("diff_conv", prep_rls diff_conv),
neuper@37954
   235
	     ("diff_sym_conv", prep_rls diff_sym_conv)
neuper@37954
   236
	     ]);
neuper@37954
   237
neuper@37954
   238
neuper@37954
   239
(** problem types **)
neuper@37954
   240
neuper@37954
   241
store_pbt
neuper@37954
   242
 (prep_pbt (theory "Diff") "pbl_fun" [] e_pblID
neuper@37954
   243
 (["function"], [], e_rls, NONE, []));
neuper@37954
   244
neuper@37954
   245
store_pbt
neuper@37954
   246
 (prep_pbt (theory "Diff") "pbl_fun_deriv" [] e_pblID
neuper@37954
   247
 (["derivative_of","function"],
neuper@37954
   248
  [("#Given" ,["functionTerm f_","differentiateFor v_"]),
neuper@37954
   249
   ("#Find"  ,["derivative f_'_"])
neuper@37954
   250
  ],
neuper@37954
   251
  append_rls "e_rls" e_rls [],
neuper@37954
   252
  SOME "Diff (f_, v_)", [["diff","differentiate_on_R"],
neuper@37954
   253
			 ["diff","after_simplification"]]));
neuper@37954
   254
neuper@37954
   255
(*here "named" is used differently from Integration"*)
neuper@37954
   256
store_pbt
neuper@37954
   257
 (prep_pbt (theory "Diff") "pbl_fun_deriv_nam" [] e_pblID
neuper@37954
   258
 (["named","derivative_of","function"],
neuper@37954
   259
  [("#Given" ,["functionEq f_","differentiateFor v_"]),
neuper@37954
   260
   ("#Find"  ,["derivativeEq f_'_"])
neuper@37954
   261
  ],
neuper@37954
   262
  append_rls "e_rls" e_rls [],
neuper@37954
   263
  SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));
neuper@37954
   264
neuper@37954
   265
neuper@37954
   266
(** methods **)
neuper@37954
   267
neuper@37954
   268
store_met
neuper@37954
   269
 (prep_met (theory "Diff") "met_diff" [] e_metID
neuper@37954
   270
 (["diff"], [],
neuper@37954
   271
   {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37954
   272
    crls = Atools_erls, nrls = norm_diff}, "empty_script"));
neuper@37954
   273
neuper@37954
   274
store_met
neuper@37954
   275
 (prep_met (theory "Diff") "met_diff_onR" [] e_metID
neuper@37954
   276
 (["diff","differentiate_on_R"],
neuper@37954
   277
   [("#Given" ,["functionTerm f_","differentiateFor v_"]),
neuper@37954
   278
    ("#Find"  ,["derivative f_'_"])
neuper@37954
   279
    ],
neuper@37954
   280
   {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, 
neuper@37954
   281
    prls=e_rls, crls = Atools_erls, nrls = norm_diff},
neuper@37954
   282
"Script DiffScr (f_::real) (v_::real) =                          " ^
neuper@37954
   283
" (let f'_ = Take (d_d v_ f_)                                    " ^
neuper@37954
   284
" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@    " ^
neuper@37954
   285
" (Repeat                                                        " ^
neuper@37954
   286
"   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or " ^
neuper@37954
   287
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
neuper@37954
   288
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or " ^
neuper@37954
   289
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or " ^
neuper@37954
   290
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or " ^
neuper@37954
   291
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or " ^
neuper@37954
   292
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or " ^
neuper@37954
   293
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or " ^
neuper@37954
   294
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or " ^
neuper@37954
   295
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or " ^
neuper@37954
   296
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or " ^
neuper@37954
   297
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or " ^
neuper@37954
   298
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or " ^
neuper@37954
   299
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or " ^
neuper@37954
   300
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or " ^
neuper@37954
   301
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or " ^
neuper@37954
   302
"    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
neuper@37954
   303
" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
neuper@37954
   304
));
neuper@37954
   305
neuper@37954
   306
store_met
neuper@37954
   307
 (prep_met (theory "Diff") "met_diff_simpl" [] e_metID
neuper@37954
   308
 (["diff","diff_simpl"],
neuper@37954
   309
   [("#Given" ,["functionTerm f_","differentiateFor v_"]),
neuper@37954
   310
    ("#Find"  ,["derivative f_'_"])
neuper@37954
   311
    ],
neuper@37954
   312
   {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
neuper@37954
   313
    prls=e_rls, crls = Atools_erls, nrls = norm_diff},
neuper@37954
   314
"Script DiffScr (f_::real) (v_::real) =                          " ^
neuper@37954
   315
" (let f'_ = Take (d_d v_ f_)                                    " ^
neuper@37954
   316
" in ((     " ^
neuper@37954
   317
" (Repeat                                                        " ^
neuper@37954
   318
"   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or " ^
neuper@37954
   319
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
neuper@37954
   320
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or " ^
neuper@37954
   321
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or " ^
neuper@37954
   322
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or " ^
neuper@37954
   323
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or " ^
neuper@37954
   324
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or " ^
neuper@37954
   325
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or " ^
neuper@37954
   326
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or " ^
neuper@37954
   327
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or " ^
neuper@37954
   328
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or " ^
neuper@37954
   329
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or " ^
neuper@37954
   330
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or " ^
neuper@37954
   331
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or " ^
neuper@37954
   332
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or " ^
neuper@37954
   333
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or " ^
neuper@37954
   334
"    (Repeat (Rewrite_Set             make_polynomial False))))  " ^
neuper@37954
   335
" )) f'_)"
neuper@37954
   336
 ));
neuper@37954
   337
    
neuper@37954
   338
store_met
neuper@37954
   339
 (prep_met (theory "Diff") "met_diff_equ" [] e_metID
neuper@37954
   340
 (["diff","differentiate_equality"],
neuper@37954
   341
   [("#Given" ,["functionEq f_","differentiateFor v_"]),
neuper@37954
   342
   ("#Find"  ,["derivativeEq f_'_"])
neuper@37954
   343
  ],
neuper@37954
   344
   {rew_ord'="tless_true", rls' = erls_diff, calc = [], 
neuper@37954
   345
    srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
neuper@37954
   346
"Script DiffEqScr (f_::bool) (v_::real) =                          " ^
neuper@37954
   347
" (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_))            " ^
neuper@37954
   348
" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@      " ^
neuper@37954
   349
" (Repeat                                                          " ^
neuper@37954
   350
"   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or   " ^
neuper@37954
   351
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif        False)) Or   " ^
neuper@37954
   352
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or   " ^
neuper@37954
   353
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or   " ^
neuper@37954
   354
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or   " ^
neuper@37954
   355
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or   " ^
neuper@37954
   356
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or   " ^
neuper@37954
   357
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or   " ^
neuper@37954
   358
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or   " ^
neuper@37954
   359
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or   " ^
neuper@37954
   360
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or   " ^
neuper@37954
   361
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or   " ^
neuper@37954
   362
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or   " ^
neuper@37954
   363
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or   " ^
neuper@37954
   364
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or   " ^
neuper@37954
   365
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or   " ^
neuper@37954
   366
"    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or   " ^
neuper@37954
   367
"    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
neuper@37954
   368
" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
neuper@37954
   369
));
neuper@37954
   370
neuper@37954
   371
store_met
neuper@37954
   372
 (prep_met (theory "Diff") "met_diff_after_simp" [] e_metID
neuper@37954
   373
 (["diff","after_simplification"],
neuper@37954
   374
   [("#Given" ,["functionTerm f_","differentiateFor v_"]),
neuper@37954
   375
    ("#Find"  ,["derivative f_'_"])
neuper@37954
   376
    ],
neuper@37954
   377
   {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
neuper@37954
   378
    crls=Atools_erls, nrls = norm_Rational},
neuper@37954
   379
"Script DiffScr (f_::real) (v_::real) =                          " ^
neuper@37954
   380
" (let f'_ = Take (d_d v_ f_)                                    " ^
neuper@37954
   381
" in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^
neuper@37954
   382
"     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@     " ^
neuper@37954
   383
"     (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@     " ^
neuper@37954
   384
"     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
neuper@37954
   385
"     (Try (Rewrite_Set norm_Rational False))) f'_)"
neuper@37954
   386
));
neuper@37954
   387
neuper@37954
   388
neuper@37954
   389
(** CAS-commands **)
neuper@37954
   390
neuper@37954
   391
(*.handle cas-input like "Diff (a * x^3 + b, x)".*)
neuper@37954
   392
(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
neuper@37954
   393
   val [Const ("Pair", _) $ t $ bdv] = pairl;
neuper@37954
   394
   *)
neuper@37954
   395
fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
neuper@37954
   396
    [((term_of o the o (parse thy)) "functionTerm", [t]),
neuper@37954
   397
     ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
neuper@37954
   398
     ((term_of o the o (parse thy)) "derivative", 
neuper@37954
   399
      [(term_of o the o (parse thy)) "f_'_"])
neuper@37954
   400
     ]
neuper@37954
   401
  | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
neuper@37954
   402
castab := 
neuper@37954
   403
overwritel (!castab, 
neuper@37954
   404
	    [((term_of o the o (parse thy)) "Diff",  
neuper@37954
   405
	      (("Isac.thy", ["derivative_of","function"], ["no_met"]), 
neuper@37954
   406
	       argl2dtss))
neuper@37954
   407
	     ]);
neuper@37954
   408
neuper@37954
   409
(*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
neuper@37954
   410
(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
neuper@37954
   411
   val [Const ("Pair", _) $ t $ bdv] = pairl;
neuper@37954
   412
   *)
neuper@37954
   413
fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
neuper@37954
   414
    [((term_of o the o (parse thy)) "functionEq", [t]),
neuper@37954
   415
     ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
neuper@37954
   416
     ((term_of o the o (parse thy)) "derivativeEq", 
neuper@37954
   417
      [(term_of o the o (parse thy)) "f_'_::bool"])
neuper@37954
   418
     ]
neuper@37954
   419
  | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
neuper@37954
   420
castab := 
neuper@37954
   421
overwritel (!castab, 
neuper@37954
   422
	    [((term_of o the o (parse thy)) "Differentiate",  
neuper@37954
   423
	      (("Isac.thy", ["named","derivative_of","function"], ["no_met"]), 
neuper@37954
   424
	       argl2dtss))
neuper@37954
   425
	     ]);
neuper@37954
   426
*}
neuper@37954
   427
neuper@37906
   428
end