239 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
239 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
240 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
240 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
241 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
241 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
242 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, |
242 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, |
243 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
243 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
244 *****Thm ("nadd_divide_distrib", |
244 *****Thm ("add_divide_distrib", |
245 *****num_str @{thm nadd_divide_distrib}) |
245 *****num_str @{thm add_divide_distrib}) |
246 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
246 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
247 ]; |
247 ]; |
248 val simplify_Integral = |
248 val simplify_Integral = |
249 Seq {id = "simplify_Integral", preconds = []:term list, |
249 Seq {id = "simplify_Integral", preconds = []:term list, |
250 rew_ord = ("dummy_ord", dummy_ord), |
250 rew_ord = ("dummy_ord", dummy_ord), |
251 erls = Atools_erls, srls = Erls, |
251 erls = Atools_erls, srls = Erls, |
252 calc = [], (*asm_thm = [],*) |
252 calc = [], (*asm_thm = [],*) |
253 rules = [Thm ("left_distrib",num_str @{thm left_distrib}), |
253 rules = [Thm ("left_distrib",num_str @{thm left_distrib}), |
254 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
254 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
255 Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}), |
255 Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}), |
256 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
256 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
257 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
257 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
258 Rls_ norm_Rational_noadd_fractions, |
258 Rls_ norm_Rational_noadd_fractions, |
259 Rls_ order_add_mult_in, |
259 Rls_ order_add_mult_in, |
260 Rls_ discard_parentheses, |
260 Rls_ discard_parentheses, |
292 * Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
292 * Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
293 * Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
293 * Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
294 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
294 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
295 * Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, |
295 * Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, |
296 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
296 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
297 * Thm ("nadd_divide_distrib", |
297 * Thm ("add_divide_distrib", |
298 * num_str @{thm nadd_divide_distrib}) |
298 * num_str @{thm add_divide_distrib}) |
299 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
299 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
300 * ]), |
300 * ]), |
301 * Calc ("HOL.divide" ,eval_cancel "#divide_e") |
301 * Calc ("HOL.divide" ,eval_cancel "#divide_e") |
302 * ], |
302 * ], |
303 * scr = EmptyScr |
303 * scr = EmptyScr |
367 srls = e_rls, |
367 srls = e_rls, |
368 prls=e_rls, |
368 prls=e_rls, |
369 crls = Atools_erls, nrls = e_rls}, |
369 crls = Atools_erls, nrls = e_rls}, |
370 "Script IntegrationScript (f_::real) (v_v::real) = " ^ |
370 "Script IntegrationScript (f_::real) (v_v::real) = " ^ |
371 " (let t_ = Take (Integral f_ D v_v) " ^ |
371 " (let t_ = Take (Integral f_ D v_v) " ^ |
372 " in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))" |
372 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))" |
373 )); |
373 )); |
374 |
374 |
375 store_met |
375 store_met |
376 (prep_met thy "met_diffint_named" [] e_metID |
376 (prep_met thy "met_diffint_named" [] e_metID |
377 (["diff","integration","named"], |
377 (["diff","integration","named"], |
382 srls = e_rls, |
382 srls = e_rls, |
383 prls=e_rls, |
383 prls=e_rls, |
384 crls = Atools_erls, nrls = e_rls}, |
384 crls = Atools_erls, nrls = e_rls}, |
385 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^ |
385 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^ |
386 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ |
386 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ |
387 " in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^ |
387 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ |
388 " (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) " |
388 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) " |
389 )); |
389 )); |
390 *} |
390 *} |
391 |
391 |
392 end |
392 end |