1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:49:36 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:55:08 2010 +0200
1.3 @@ -79,8 +79,9 @@
1.4 use_thy "Knowledge/Trig"
1.5 use_thy "Knowledge/LogExp"
1.6 use_thy "Knowledge/Diff"
1.7 +use_thy "Knowledge/DiffApp"
1.8
1.9 -use_thy "Knowledge/DiffApp"
1.10 +use_thy "Knowledge/Integrate"
1.11
1.12 ML {* 111;
1.13 *}
1.14 @@ -88,7 +89,6 @@
1.15
1.16 text {*------------------------------------------*}
1.17 (*
1.18 -use_thy "Knowledge/Integrate"
1.19 use_thy "Knowledge/EqSystem"
1.20 use_thy "Knowledge/Biegelinie"
1.21 use_thy "Knowledge/AlgEin"
2.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:49:36 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:55:08 2010 +0200
2.3 @@ -13,9 +13,9 @@
2.4 is'_f'_x :: "real => bool" ("_ is'_f'_x" 10)
2.5
2.6 (*descriptions in the related problems*)
2.7 - integrateBy :: real => una
2.8 - antiDerivative :: real => una
2.9 - antiDerivativeName :: (real => real) => una
2.10 + integrateBy :: "real => una"
2.11 + antiDerivative :: "real => una"
2.12 + antiDerivativeName :: "(real => real) => una"
2.13
2.14 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
2.15 Integrate :: "[real * real] => real"
2.16 @@ -113,8 +113,8 @@
2.17 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
2.18 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
2.19 ]);
2.20 -
2.21 -
2.22 +*}
2.23 +ML {*
2.24 (** rulesets **)
2.25
2.26 (*.rulesets for integration.*)
2.27 @@ -143,6 +143,8 @@
2.28 Calc ("op +", eval_binop "#add_")(*for n+1*)
2.29 ],
2.30 scr = EmptyScr};
2.31 +*}
2.32 +ML {*
2.33 val add_new_c =
2.34 Seq {id="add_new_c", preconds = [],
2.35 rew_ord = ("termlessI",termlessI),
2.36 @@ -155,7 +157,7 @@
2.37 Calc ("Integrate.is'_f'_x",
2.38 eval_is_f_x "is_f_x_"),
2.39 Thm ("not_true",num_str @{thm not_true}),
2.40 - Thm ("not_false",num_str @{thm not_false)
2.41 + Thm ("not_false",num_str @{thm not_false})
2.42 ],
2.43 scr = EmptyScr},
2.44 srls = Erls, calc = [],
2.45 @@ -163,6 +165,8 @@
2.46 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
2.47 ],
2.48 scr = EmptyScr};
2.49 +*}
2.50 +ML {*
2.51
2.52 (*.rulesets for simplifying Integrals.*)
2.53
2.54 @@ -331,6 +335,8 @@
2.55 ("norm_Rational_rls_noadd_fractions",
2.56 norm_Rational_rls_noadd_fractions)
2.57 ]);
2.58 +*}
2.59 +ML {*
2.60
2.61 (** problems **)
2.62
2.63 @@ -338,7 +344,7 @@
2.64 (prep_pbt thy "pbl_fun_integ" [] e_pblID
2.65 (["integrate","function"],
2.66 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.67 - ("#Find" ,["antiDerivative F_"])
2.68 + ("#Find" ,["antiDerivative F_F"])
2.69 ],
2.70 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.71 SOME "Integrate (f_f, v_v)",
2.72 @@ -349,43 +355,47 @@
2.73 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
2.74 (["named","integrate","function"],
2.75 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.76 - ("#Find" ,["antiDerivativeName F_"])
2.77 + ("#Find" ,["antiDerivativeName F_F"])
2.78 ],
2.79 append_rls "e_rls" e_rls [(*for preds in where_*)],
2.80 SOME "Integrate (f_f, v_v)",
2.81 [["diff","integration","named"]]));
2.82
2.83 +*}
2.84 +ML {*
2.85 (** methods **)
2.86
2.87 store_met
2.88 (prep_met thy "met_diffint" [] e_metID
2.89 (["diff","integration"],
2.90 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.91 - ("#Find" ,["antiDerivative F_"])
2.92 + ("#Find" ,["antiDerivative F_F"])
2.93 ],
2.94 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
2.95 srls = e_rls,
2.96 prls=e_rls,
2.97 crls = Atools_erls, nrls = e_rls},
2.98 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
2.99 -" (let t_ = Take (Integral f_ D v_v) " ^
2.100 -" in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
2.101 +" (let t_t = Take (Integral f_f D v_v) " ^
2.102 +" in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"
2.103 ));
2.104 -
2.105 + *}
2.106 +ML {*
2.107 +
2.108 store_met
2.109 (prep_met thy "met_diffint_named" [] e_metID
2.110 (["diff","integration","named"],
2.111 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.112 - ("#Find" ,["antiDerivativeName F_"])
2.113 + ("#Find" ,["antiDerivativeName F_F"])
2.114 ],
2.115 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
2.116 srls = e_rls,
2.117 prls=e_rls,
2.118 crls = Atools_erls, nrls = e_rls},
2.119 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^
2.120 -" (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^
2.121 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
2.122 +" (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
2.123 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
2.124 -" (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) "
2.125 +" (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) "
2.126 ));
2.127 *}
2.128