34 |
34 |
35 |
35 |
36 "----------- parsing ---------------------------------------------"; |
36 "----------- parsing ---------------------------------------------"; |
37 "----------- parsing ---------------------------------------------"; |
37 "----------- parsing ---------------------------------------------"; |
38 "----------- parsing ---------------------------------------------"; |
38 "----------- parsing ---------------------------------------------"; |
39 fun str2t str = (term_of o the o (parse Integrate.thy)) str; |
39 fun str2term str = (term_of o the o (parse Integrate.thy)) str; |
40 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t; |
40 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t; |
41 |
41 |
42 val t = str2t "Integral x D x"; |
42 val t = str2term "Integral x D x"; |
43 val t = str2t "Integral x^^^2 D x"; |
43 val t = str2term "Integral x^^^2 D x"; |
44 atomty t; |
44 atomty t; |
45 |
45 |
46 val t = str2t "ff x is_f_x"; |
46 val t = str2term "ff x is_f_x"; |
47 case t of Const ("Integrate.is'_f'_x", _) $ _ => () |
47 case t of Const ("Integrate.is'_f'_x", _) $ _ => () |
48 | _ => raise error "integrate.sml: parsing: ff x is_f_x"; |
48 | _ => raise error "integrate.sml: parsing: ff x is_f_x"; |
49 |
49 |
50 |
50 |
51 "----------- integrate by rewriting ------------------------------"; |
51 "----------- integrate by rewriting ------------------------------"; |
62 eval_occurs_in "#occurs_in_"), |
62 eval_occurs_in "#occurs_in_"), |
63 Thm ("not_true",num_str not_true), |
63 Thm ("not_true",num_str not_true), |
64 Thm ("not_false",not_false) |
64 Thm ("not_false",not_false) |
65 ], |
65 ], |
66 scr = EmptyScr}; |
66 scr = EmptyScr}; |
67 val subs = [(str2t "bdv", str2t "x")]; |
67 val subs = [(str2term "bdv", str2term "x")]; |
68 fun rewrit thm str = |
68 fun rewrit thm str = |
69 fst (the (rewrite_inst_ Integrate.thy tless_true |
69 fst (the (rewrite_inst_ Integrate.thy tless_true |
70 conditions_in_integration_rules |
70 conditions_in_integration_rules |
71 true subs thm str)); |
71 true subs thm str)); |
72 val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str; |
72 val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str; |
73 val str = rewrit integral_const (str2t "Integral M'/EJ D x"); term2s str; |
73 val str = rewrit integral_const (str2term "Integral M'/EJ D x"); term2s str; |
74 val str = (rewrit integral_const (str2t "Integral x D x")) |
74 val str = (rewrit integral_const (str2term "Integral x D x")) |
75 handle OPTION => str2t "no_rewrite"; |
75 handle OPTION => str2term "no_rewrite"; |
76 |
76 |
77 val str = rewrit integral_var (str2t "Integral x D x"); term2s str; |
77 val str = rewrit integral_var (str2term "Integral x D x"); term2s str; |
78 val str = (rewrit integral_var (str2t "Integral a D x")) |
78 val str = (rewrit integral_var (str2term "Integral a D x")) |
79 handle OPTION => str2t "no_rewrite"; |
79 handle OPTION => str2term "no_rewrite"; |
80 |
80 |
81 val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str; |
81 val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str; |
82 |
82 |
83 val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str; |
83 val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str; |
84 val str = (rewrit integral_mult (str2t "Integral x * x D x")) |
84 val str = (rewrit integral_mult (str2term "Integral x * x D x")) |
85 handle OPTION => str2t "no_rewrite"; |
85 handle OPTION => str2term "no_rewrite"; |
86 |
86 |
87 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str; |
87 val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str; |
88 |
88 |
89 |
89 |
90 "----------- test add_new_c, is_f_x ------------------------------"; |
90 "----------- test add_new_c, is_f_x ------------------------------"; |
91 "----------- test add_new_c, is_f_x ------------------------------"; |
91 "----------- test add_new_c, is_f_x ------------------------------"; |
92 "----------- test add_new_c, is_f_x ------------------------------"; |
92 "----------- test add_new_c, is_f_x ------------------------------"; |
110 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then () |
110 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then () |
111 else raise error "intergrate.sml: diff. rewrite_set add_new_c 2"; |
111 else raise error "intergrate.sml: diff. rewrite_set add_new_c 2"; |
112 |
112 |
113 |
113 |
114 (*WN080222 replace call_new_c with add_new_c---------------------- |
114 (*WN080222 replace call_new_c with add_new_c---------------------- |
115 val term = str2t "new_c (c * x^^^2 + c_2)"; |
115 val term = str2term "new_c (c * x^^^2 + c_2)"; |
116 val Some (_,t') = eval_new_c 0 0 term 0; |
116 val Some (_,t') = eval_new_c 0 0 term 0; |
117 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then () |
117 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then () |
118 else raise error "integrate.sml: eval_new_c ???"; |
118 else raise error "integrate.sml: eval_new_c ???"; |
119 |
119 |
120 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)"; |
120 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)"; |
121 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; |
121 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; |
122 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then () |
122 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then () |
123 else raise error "integrate.sml: matches new_c = False"; |
123 else raise error "integrate.sml: matches new_c = False"; |
124 |
124 |
125 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)"; |
125 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)"; |
126 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; |
126 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; |
127 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True" |
127 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True" |
128 then () else raise error "integrate.sml: matches new_c = True"; |
128 then () else raise error "integrate.sml: matches new_c = True"; |
129 |
129 |
130 val t = str2t "ff x is_f_x"; |
130 val t = str2term "ff x is_f_x"; |
131 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; |
131 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; |
132 if term2s t' = "(ff x is_f_x) = True" then () |
132 if term2s t' = "(ff x is_f_x) = True" then () |
133 else raise error "integrate.sml: eval_is_f_x --> true"; |
133 else raise error "integrate.sml: eval_is_f_x --> true"; |
134 |
134 |
135 val t = str2t "q_0/2 * L * x is_f_x"; |
135 val t = str2term "q_0/2 * L * x is_f_x"; |
136 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; |
136 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; |
137 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then () |
137 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then () |
138 else raise error "integrate.sml: eval_is_f_x --> false"; |
138 else raise error "integrate.sml: eval_is_f_x --> false"; |
139 |
139 |
140 val conditions_in_integration = |
140 val conditions_in_integration = |
151 ], |
151 ], |
152 scr = EmptyScr}; |
152 scr = EmptyScr}; |
153 fun rewrit thm t = |
153 fun rewrit thm t = |
154 fst (the (rewrite_inst_ Integrate.thy tless_true |
154 fst (the (rewrite_inst_ Integrate.thy tless_true |
155 conditions_in_integration true subs thm t)); |
155 conditions_in_integration true subs thm t)); |
156 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t; |
156 val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t; |
157 val t = (rewrit call_for_new_c t) |
157 val t = (rewrit call_for_new_c t) |
158 handle OPTION => str2t "no_rewrite"; |
158 handle OPTION => str2term "no_rewrite"; |
159 |
159 |
160 val t = rewrit call_for_new_c |
160 val t = rewrit call_for_new_c |
161 (str2t "ff x = q_0/2 *L*x"); term2s t; |
161 (str2term "ff x = q_0/2 *L*x"); term2s t; |
162 val t = (rewrit call_for_new_c |
162 val t = (rewrit call_for_new_c |
163 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x")) |
163 (str2term "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x")) |
164 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite"; |
164 handle OPTION => (*NOT: + new_c ..=..!!*)str2term "no_rewrite"; |
165 --------------------------------------------------------------------*) |
165 --------------------------------------------------------------------*) |
166 |
166 |
167 |
167 |
168 "----------- simplify by ruleset reducing make_ratpoly_in --------"; |
168 "----------- simplify by ruleset reducing make_ratpoly_in --------"; |
169 "----------- simplify by ruleset reducing make_ratpoly_in --------"; |
169 "----------- simplify by ruleset reducing make_ratpoly_in --------"; |
345 val {scr = Script sc,... } = get_met ["diff","integration","named"]; |
345 val {scr = Script sc,... } = get_met ["diff","integration","named"]; |
346 val [_,_, F2_] = formal_args sc; |
346 val [_,_, F2_] = formal_args sc; |
347 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's"; |
347 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's"; |
348 |
348 |
349 val ((dsc as Const ("Integrate.antiDerivativeName", _)) |
349 val ((dsc as Const ("Integrate.antiDerivativeName", _)) |
350 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff"; |
350 $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff"; |
351 if is_dsc dsc then () else raise error "integrate.sml: no description"; |
351 if is_dsc dsc then () else raise error "integrate.sml: no description"; |
352 if F1_type = F3_type then () |
352 if F1_type = F3_type then () |
353 else raise error "integrate.sml: unequal types in find's"; |
353 else raise error "integrate.sml: unequal types in find's"; |
354 |
354 |
355 show_ptyps(); |
355 show_ptyps(); |