Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Diff.thy
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37983 03bfbc480107
child 37993 e4796b1125fb
equal deleted inserted replaced
37990:24609758d219 37991:028442673981 
   281     ],
 
   281     ],
 
   282    {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, 
   282    {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, 
   283     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
 
   283     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
 
   284 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   284 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   285 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   285 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   286 " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@    " ^
 
   286 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@    " ^
 
   287 " (Repeat                                                        " ^
 
   287 " (Repeat                                                        " ^
 
   288 "   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or " ^
 
   288 "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^
 
   289 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
 
   289 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
 
   290 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or " ^
 
   290 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^
 
   291 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or " ^
 
   291 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or " ^
 
   292 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or " ^
 
   292 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^
 
   293 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or " ^
 
   293 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^
 
   294 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or " ^
 
   294 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^
 
   295 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or " ^
 
   295 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^
 
   296 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or " ^
 
   296 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^
 
   297 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or " ^
 
   297 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^
 
   298 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or " ^
 
   298 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^
 
   299 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or " ^
 
   299 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^
 
   300 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or " ^
 
   300 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^
 
   301 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or " ^
 
   301 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^
 
   302 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or " ^
 
   302 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
 
   303 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or " ^
 
   303 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
 
   304 "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
 
   304 "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
 
   305 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
 
   305 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
 
   306 ));
 
   306 ));
 
   307 
   307 
   308 store_met
 
   308 store_met
 
   309  (prep_met thy "met_diff_simpl" [] e_metID
 
   309  (prep_met thy "met_diff_simpl" [] e_metID
 
   310  (["diff","diff_simpl"],
 
   310  (["diff","diff_simpl"],
 
   315     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
 
   315     prls=e_rls, crls = Atools_erls, nrls = norm_diff},
 
   316 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   316 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   317 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   317 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   318 " in ((     " ^
 
   318 " in ((     " ^
 
   319 " (Repeat                                                        " ^
 
   319 " (Repeat                                                        " ^
 
   320 "   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or " ^
 
   320 "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or " ^
 
   321 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
 
   321 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
 
   322 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or " ^
 
   322 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or " ^
 
   323 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or " ^
 
   323 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or " ^
 
   324 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or " ^
 
   324 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or " ^
 
   325 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or " ^
 
   325 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or " ^
 
   326 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or " ^
 
   326 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or " ^
 
   327 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or " ^
 
   327 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or " ^
 
   328 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or " ^
 
   328 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or " ^
 
   329 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or " ^
 
   329 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or " ^
 
   330 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or " ^
 
   330 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or " ^
 
   331 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or " ^
 
   331 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or " ^
 
   332 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or " ^
 
   332 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or " ^
 
   333 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or " ^
 
   333 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or " ^
 
   334 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or " ^
 
   334 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
 
   335 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or " ^
 
   335 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
 
   336 "    (Repeat (Rewrite_Set             make_polynomial False))))  " ^
 
   336 "    (Repeat (Rewrite_Set             make_polynomial False))))  " ^
 
   337 " )) f'_)"
 
   337 " )) f'_)"
 
   338  ));
 
   338  ));
 
   339     
   339     
   340 store_met
 
   340 store_met
 
   345   ],
 
   345   ],
 
   346    {rew_ord'="tless_true", rls' = erls_diff, calc = [], 
   346    {rew_ord'="tless_true", rls' = erls_diff, calc = [], 
   347     srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
 
   347     srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
 
   348 "Script DiffEqScr (f_::bool) (v_v::real) =                          " ^
 
   348 "Script DiffEqScr (f_::bool) (v_v::real) =                          " ^
 
   349 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_))            " ^
 
   349 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_))            " ^
 
   350 " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@      " ^
 
   350 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@      " ^
 
   351 " (Repeat                                                          " ^
 
   351 " (Repeat                                                          " ^
 
   352 "   ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum        False)) Or   " ^
 
   352 "   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or   " ^
 
   353 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif        False)) Or   " ^
 
   353 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif        False)) Or   " ^
 
   354 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or   " ^
 
   354 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or   " ^
 
   355 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or   " ^
 
   355 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or   " ^
 
   356 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or   " ^
 
   356 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or   " ^
 
   357 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or   " ^
 
   357 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or   " ^
 
   358 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or   " ^
 
   358 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or   " ^
 
   359 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or   " ^
 
   359 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or   " ^
 
   360 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or   " ^
 
   360 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or   " ^
 
   361 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or   " ^
 
   361 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or   " ^
 
   362 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or   " ^
 
   362 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or   " ^
 
   363 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or   " ^
 
   363 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or   " ^
 
   364 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or   " ^
 
   364 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or   " ^
 
   365 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or   " ^
 
   365 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or   " ^
 
   366 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or   " ^
 
   366 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or   " ^
 
   367 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or   " ^
 
   367 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or   " ^
 
   368 "    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        False)) Or   " ^
 
   368 "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or   " ^
 
   369 "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
 
   369 "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
 
   370 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
 
   370 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
 
   371 ));
 
   371 ));
 
   372 
   372 
   373 store_met
 
   373 store_met
 
   374  (prep_met thy "met_diff_after_simp" [] e_metID
 
   374  (prep_met thy "met_diff_after_simp" [] e_metID
 
   375  (["diff","after_simplification"],
 
   375  (["diff","after_simplification"],
 
   379    {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
 
   379    {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
 
   380     crls=Atools_erls, nrls = norm_Rational},
 
   380     crls=Atools_erls, nrls = norm_Rational},
 
   381 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   381 "Script DiffScr (f_::real) (v_v::real) =                          " ^
 
   382 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   382 " (let f'_ = Take (d_d v_v f_)                                    " ^
 
   383 " in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^
 
   383 " in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^
 
   384 "     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@     " ^
 
   384 "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@     " ^
 
   385 "     (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@     " ^
 
   385 "     (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@     " ^
 
   386 "     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
 
   386 "     (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
 
   387 "     (Try (Rewrite_Set norm_Rational False))) f'_)"
 
   387 "     (Try (Rewrite_Set norm_Rational False))) f'_)"
 
   388 ));
 
   388 ));
 
   389 
   389 
   390 
   390 
   391 (** CAS-commands **)
 
   391 (** CAS-commands **)
 
   402      ]
 
   402      ]
 
   403   | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
 
   403   | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
 
   404 castab := 
   404 castab := 
   405 overwritel (!castab, 
   405 overwritel (!castab, 
   406 	    [((term_of o the o (parse thy)) "Diff",  
   406 	    [((term_of o the o (parse thy)) "Diff",  
   407 	      (("Isac.thy", ["derivative_of","function"], ["no_met"]), 
   407 	      (("Isac", ["derivative_of","function"], ["no_met"]), 
   408 	       argl2dtss))
 
   408 	       argl2dtss))
 
   409 	     ]);
 
   409 	     ]);
 
   410 
   410 
   411 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
 
   411 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
 
   412 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
 
   412 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
 
   420      ]
 
   420      ]
 
   421   | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
 
   421   | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
 
   422 castab := 
   422 castab := 
   423 overwritel (!castab, 
   423 overwritel (!castab, 
   424 	    [((term_of o the o (parse thy)) "Differentiate",  
   424 	    [((term_of o the o (parse thy)) "Differentiate",  
   425 	      (("Isac.thy", ["named","derivative_of","function"], ["no_met"]), 
   425 	      (("Isac", ["named","derivative_of","function"], ["no_met"]), 
   426 	       argl2dtss))
 
   426 	       argl2dtss))
 
   427 	     ]);
 
   427 	     ]);
 
   428 *}
 
   428 *}
 
   429 
   429 
   430 end
 
   430 end
wneuper/isa