1 (* tools for integration over the reals
4 (c) due to copyright terms
6 use"~/proto2/isac/src/sml/IsacKnowledge/Integrate.ML";
9 (** interface isabelle -- isac **)
11 theory' := overwritel (!theory', [("Integrate.thy",Integrate.thy)]);
13 theorem' := overwritel (!theorem',
14 [("integral_const",num_str integral_const),
15 ("integral_var",num_str integral_var),
16 ("integral_add",num_str integral_add),
17 ("integral_mult",num_str integral_mult),
18 ("call_for_new_c",num_str call_for_new_c),
19 ("integral_pow",num_str integral_pow)
22 (** eval functions **)
24 val c = Free ("c", HOLogic.realT);
25 (*.create a new unique variable 'c..' in a term.*)
28 case (explode o id_of) var of
30 | "c"::"_"::is => (case (int_of_str o implode) is of
34 fun get_coeff c = case (explode o id_of) c of
35 "c"::"_"::is => (the o int_of_str o implode) is
37 val cs = filter selc (vars term);
41 | [c] => Free ("c_2", HOLogic.realT)
43 let val max_coeff = maxl (map get_coeff cs)
44 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
47 (*("new_c", ("Integrate.new'_c", eval_new_c "new_c_"))*)
48 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
49 Some ((term2str p) ^ " = " ^ term2str (new_c p),
50 Trueprop $ (mk_equality (p, new_c p)))
51 | eval_new_c _ _ _ _ = None;
53 calclist':= overwritel (!calclist',
54 [("new_c", ("Integrate.new'_c", eval_new_c "new_c_"))
59 val integration_rules =
60 prep_rls (Rls {id="integration_rules", preconds = [],
61 rew_ord = ("termlessI",termlessI),
62 erls = Rls {id="conditions_in_integration_rules",
64 rew_ord = ("termlessI",termlessI),
66 srls = Erls, calc = [],
67 rules = [(*for rewriting conditions in Thm's*)
68 Calc ("Atools.occurs'_in",
69 eval_occurs_in "#occurs_in_"),
70 Thm ("not_true",num_str not_true),
71 Thm ("not_false",not_false)
74 srls = Erls, calc = [],
76 Thm ("integral_const",num_str integral_const),
77 Thm ("integral_var",num_str integral_var),
78 Thm ("integral_add",num_str integral_add),
79 Thm ("integral_mult",num_str integral_mult),
80 Thm ("integral_pow",num_str integral_pow),
81 Calc ("op +", eval_binop "#add_")(*for n+1*)
85 prep_rls (Seq {id="add_new_c", preconds = [],
86 rew_ord = ("termlessI",termlessI),
87 erls = Rls {id="conditions_in_add_new_c",
89 rew_ord = ("termlessI",termlessI),
91 srls = Erls, calc = [],
92 rules = [Calc ("Tools.matches", eval_matches""),
93 Thm ("not_true",num_str not_true),
94 Thm ("not_false",num_str not_false)
97 srls = Erls, calc = [],
98 rules = [ Thm ("call_for_new_c", num_str call_for_new_c),
99 Calc("Integrate.new'_c", eval_new_c "new_c_")
103 prep_rls (Seq {id="integration", preconds = [],
104 rew_ord = ("termlessI",termlessI),
105 erls = Rls {id="conditions_in_integration",
107 rew_ord = ("termlessI",termlessI),
109 srls = Erls, calc = [],
112 srls = Erls, calc = [],
113 rules = [ Rls_ integration_rules,
118 ruleset' := overwritel (!ruleset', [("integration_rules", integration_rules),
119 ("add_new_c", add_new_c),
120 ("integration", integration)]);
125 (prep_pbt Integrate.thy
126 (["integrate","function"],
127 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
128 ("#Find" ,["antiDerivative F_"])
130 append_rls "e_rls" e_rls [(*for preds in where_*)],
131 Some "Integrate (f_, v_)",
132 [["Diff","integration"]]));
135 (prep_pbt Integrate.thy
136 (["named","integrate","function"],
137 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
138 ("#Find" ,["antiDerivative F_"])
140 append_rls "e_rls" e_rls [(*for preds in where_*)],
141 Some "Integrate (f_, v_)",
142 [["Diff","integration","named"]]));
147 (prep_met Integrate.thy
148 (["Diff","integration"],
149 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
150 ("#Find" ,["antiDerivative F_"])
152 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
155 crls = Atools_erls, nrls = e_rls},
156 "Script IntegrationScript (f_::real) (v_::real) = \
157 \ (let t_ = Integral f_ D v_ \
158 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
162 (prep_met Integrate.thy
163 (["Diff","integration","named"],
164 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
165 ("#Find" ,["antiDerivative F_"])
167 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
170 crls = Atools_erls, nrls = e_rls},
171 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
172 \ (let t_ = (F_ = Integral f_ D v_) \
173 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"