wneuper/isa: comparison src/Tools/isac/Knowledge/Integrate.thy

equal deleted inserted replaced

-:fac82f29f143
+:eb7d9cbaa3ef
 Integral            :: "[real, real]=> real" ("Integral _ D _" 91)
 (*new'_c	      :: "real => real"        ("new'_c _" 66)*)
 is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)
 (*descriptions in the related problems*)
-integrateBy         :: real => una
+integrateBy         :: "real => una"
-antiDerivative      :: real => una
+antiDerivative      :: "real => una"
-antiDerivativeName  :: (real => real) => una
+antiDerivativeName  :: "(real => real) => una"
 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
 Integrate           :: "[real * real] => real"
 (*Script-names*)
 calclist':= overwritel (!calclist',
 [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
 ]);
+*}
+ML {*
 (** rulesets **)
 (*.rulesets for integration.*)
 val integration_rules =
 Rls {id="integration_rules", preconds = [],
 		  Thm ("integral_mult",num_str @{thm integral_mult}),
 		  Thm ("integral_pow",num_str @{thm integral_pow}),
 		  Calc ("op +", eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = EmptyScr};
+*}
+ML {*
 val add_new_c =
 Seq {id="add_new_c", preconds = [],
 	 rew_ord = ("termlessI",termlessI),
 	 erls = Rls {id="conditions_in_add_new_c",
 		     preconds = [],
 		     srls = Erls, calc = [],
 		     rules = [Calc ("Tools.matches", eval_matches""),
 			      Calc ("Integrate.is'_f'_x",
 				    eval_is_f_x "is_f_x_"),
 			      Thm ("not_true",num_str @{thm not_true}),
-			      Thm ("not_false",num_str @{thm not_false)
+			      Thm ("not_false",num_str @{thm not_false})
 			      ],
 		     scr = EmptyScr},
 	 srls = Erls, calc = [],
 	 rules = [ (*Thm ("call_for_new_c", num_str @{thm call_for_new_c}),*)
 		   Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
 		   ],
 	 scr = EmptyScr};
+*}
+ML {*
 (*.rulesets for simplifying Integrals.*)
 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
 val norm_Rational_rls_noadd_fractions =
 	     ("separate_bdv2", separate_bdv2),
 	     ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
 	     ("norm_Rational_rls_noadd_fractions",
 	      norm_Rational_rls_noadd_fractions)
 	     ]);
+*}
+ML {*
 (** problems **)
 store_pbt
 (prep_pbt thy "pbl_fun_integ" [] e_pblID
 (["integrate","function"],
 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-("#Find"  ,["antiDerivative F_"])
+("#Find"  ,["antiDerivative F_F"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
 SOME "Integrate (f_f, v_v)",
 [["diff","integration"]]));
 (*here "named" is used differently from Differentiation"*)
 store_pbt
 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
 (["named","integrate","function"],
 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-("#Find"  ,["antiDerivativeName F_"])
+("#Find"  ,["antiDerivativeName F_F"])
 ],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
 SOME "Integrate (f_f, v_v)",
 [["diff","integration","named"]]));
+*}
+ML {*
 (** methods **)
 store_met
 (prep_met thy "met_diffint" [] e_metID
 	      (["diff","integration"],
 	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-		("#Find"  ,["antiDerivative F_"])
+		("#Find"  ,["antiDerivative F_F"])
 		],
 	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
 		srls = e_rls,
 		prls=e_rls,
 	     crls = Atools_erls, nrls = e_rls},
 "Script IntegrationScript (f_f::real) (v_v::real) =                " ^
-"  (let t_ = Take (Integral f_ D v_v)                             " ^
+"  (let t_t = Take (Integral f_f D v_v)                             " ^
-"   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
+"   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"
 ));
+*}
+ML {*
 store_met
 (prep_met thy "met_diffint_named" [] e_metID
 	      (["diff","integration","named"],
 	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-		("#Find"  ,["antiDerivativeName F_"])
+		("#Find"  ,["antiDerivativeName F_F"])
 		],
 	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
 		srls = e_rls,
 		prls=e_rls,
 		crls = Atools_erls, nrls = e_rls},
-"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^
+"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
-"  (let t_ = Take (F_ v_v = Integral f_ D v_v)                            " ^
+"  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
 "   in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@  " ^
-"       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_)            "
+"       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t)            "
 ));
 *}
 end

branch	isac-update-Isa09-2
changeset 37996	eb7d9cbaa3ef
parent 37994	eb4c556a525b
child 38014	3e11e3c2dc42