|
1 (* SML functions for rational arithmetic |
|
2 WN.22.10.99 |
|
3 use"../knowledge/Test.ML"; |
|
4 use"Knowledge/Test.ML"; |
|
5 use"Test.ML"; |
|
6 *) |
|
7 |
|
8 |
|
9 (** interface isabelle -- isac **) |
|
10 |
|
11 theory' := overwritel (!theory', [("Test.thy",Test.thy)]); |
|
12 |
|
13 (** evaluation of numerals and predicates **) |
|
14 |
|
15 (*does a term contain a root ?*) |
|
16 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = |
|
17 if strip_thy op0 <> "is'_root'_free" |
|
18 then raise error ("eval_root_free: wrong "^op0) |
|
19 else if const_in (strip_thy op0) arg |
|
20 then SOME (mk_thmid thmid "" |
|
21 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
22 Trueprop $ (mk_equality (t, false_as_term))) |
|
23 else SOME (mk_thmid thmid "" |
|
24 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
25 Trueprop $ (mk_equality (t, true_as_term))) |
|
26 | eval_root_free _ _ _ _ = NONE; |
|
27 |
|
28 (*does a term contain a root ?*) |
|
29 fun eval_contains_root (thmid:string) _ |
|
30 (t as (Const("Test.contains'_root",t0) $ arg)) thy = |
|
31 if member op = (ids_of arg) "sqrt" |
|
32 then SOME (mk_thmid thmid "" |
|
33 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
34 Trueprop $ (mk_equality (t, true_as_term))) |
|
35 else SOME (mk_thmid thmid "" |
|
36 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
37 Trueprop $ (mk_equality (t, false_as_term))) |
|
38 | eval_contains_root _ _ _ _ = NONE; |
|
39 |
|
40 calclist':= overwritel (!calclist', |
|
41 [("is_root_free", ("Test.is'_root'_free", |
|
42 eval_root_free"#is_root_free_")), |
|
43 ("contains_root", ("Test.contains'_root", |
|
44 eval_contains_root"#contains_root_")) |
|
45 ]); |
|
46 |
|
47 (** term order **) |
|
48 fun term_order (_:subst) tu = (term_ordI [] tu = LESS); |
|
49 |
|
50 (** rule sets **) |
|
51 |
|
52 val testerls = |
|
53 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), |
|
54 erls = e_rls, srls = Erls, |
|
55 calc = [], |
|
56 rules = [Thm ("refl",num_str refl), |
|
57 Thm ("le_refl",num_str le_refl), |
|
58 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
59 Thm ("not_true",num_str not_true), |
|
60 Thm ("not_false",num_str not_false), |
|
61 Thm ("and_true",and_true), |
|
62 Thm ("and_false",and_false), |
|
63 Thm ("or_true",or_true), |
|
64 Thm ("or_false",or_false), |
|
65 Thm ("and_commute",num_str and_commute), |
|
66 Thm ("or_commute",num_str or_commute), |
|
67 |
|
68 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
69 Calc ("Tools.matches",eval_matches ""), |
|
70 |
|
71 Calc ("op +",eval_binop "#add_"), |
|
72 Calc ("op *",eval_binop "#mult_"), |
|
73 Calc ("Atools.pow" ,eval_binop "#power_"), |
|
74 |
|
75 Calc ("op <",eval_equ "#less_"), |
|
76 Calc ("op <=",eval_equ "#less_equal_"), |
|
77 |
|
78 Calc ("Atools.ident",eval_ident "#ident_")], |
|
79 scr = Script ((term_of o the o (parse thy)) |
|
80 "empty_script") |
|
81 }:rls; |
|
82 |
|
83 (*.for evaluation of conditions in rewrite rules.*) |
|
84 (*FIXXXXXXME 10.8.02: handle like _simplify*) |
|
85 val tval_rls = |
|
86 Rls{id = "tval_rls", preconds = [], |
|
87 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), |
|
88 erls=testerls,srls = e_rls, |
|
89 calc=[], |
|
90 rules = [Thm ("refl",num_str refl), |
|
91 Thm ("le_refl",num_str le_refl), |
|
92 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
93 Thm ("not_true",num_str not_true), |
|
94 Thm ("not_false",num_str not_false), |
|
95 Thm ("and_true",and_true), |
|
96 Thm ("and_false",and_false), |
|
97 Thm ("or_true",or_true), |
|
98 Thm ("or_false",or_false), |
|
99 Thm ("and_commute",num_str and_commute), |
|
100 Thm ("or_commute",num_str or_commute), |
|
101 |
|
102 Thm ("real_diff_minus",num_str real_diff_minus), |
|
103 |
|
104 Thm ("root_ge0",num_str root_ge0), |
|
105 Thm ("root_add_ge0",num_str root_add_ge0), |
|
106 Thm ("root_ge0_1",num_str root_ge0_1), |
|
107 Thm ("root_ge0_2",num_str root_ge0_2), |
|
108 |
|
109 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
110 Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"), |
|
111 Calc ("Tools.matches",eval_matches ""), |
|
112 Calc ("Test.contains'_root", |
|
113 eval_contains_root"#contains_root_"), |
|
114 |
|
115 Calc ("op +",eval_binop "#add_"), |
|
116 Calc ("op *",eval_binop "#mult_"), |
|
117 Calc ("Root.sqrt",eval_sqrt "#sqrt_"), |
|
118 Calc ("Atools.pow" ,eval_binop "#power_"), |
|
119 |
|
120 Calc ("op <",eval_equ "#less_"), |
|
121 Calc ("op <=",eval_equ "#less_equal_"), |
|
122 |
|
123 Calc ("Atools.ident",eval_ident "#ident_")], |
|
124 scr = Script ((term_of o the o (parse thy)) |
|
125 "empty_script") |
|
126 }:rls; |
|
127 |
|
128 |
|
129 ruleset' := overwritelthy thy (!ruleset', |
|
130 [("testerls", prep_rls testerls) |
|
131 ]); |
|
132 |
|
133 |
|
134 (*make () dissappear*) |
|
135 val rearrange_assoc = |
|
136 Rls{id = "rearrange_assoc", preconds = [], |
|
137 rew_ord = ("e_rew_ord",e_rew_ord), |
|
138 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*) |
|
139 rules = |
|
140 [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)), |
|
141 Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))], |
|
142 scr = Script ((term_of o the o (parse thy)) |
|
143 "empty_script") |
|
144 }:rls; |
|
145 |
|
146 val ac_plus_times = |
|
147 Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order), |
|
148 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*) |
|
149 rules = |
|
150 [Thm ("radd_commute",radd_commute), |
|
151 Thm ("radd_left_commute",radd_left_commute), |
|
152 Thm ("radd_assoc",radd_assoc), |
|
153 Thm ("rmult_commute",rmult_commute), |
|
154 Thm ("rmult_left_commute",rmult_left_commute), |
|
155 Thm ("rmult_assoc",rmult_assoc)], |
|
156 scr = Script ((term_of o the o (parse thy)) |
|
157 "empty_script") |
|
158 }:rls; |
|
159 |
|
160 (*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*) |
|
161 val norm_equation = |
|
162 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), |
|
163 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*) |
|
164 rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add) |
|
165 ], |
|
166 scr = Script ((term_of o the o (parse thy)) |
|
167 "empty_script") |
|
168 }:rls; |
|
169 |
|
170 (** rule sets **) |
|
171 |
|
172 val STest_simplify = (* vv--- not changed to real by parse*) |
|
173 "Script STest_simplify (t_::'z) = \ |
|
174 \(Repeat\ |
|
175 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
|
176 \ (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ \ |
|
177 \ (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ \ |
|
178 \ (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@\ |
|
179 \ (Try (Repeat (Rewrite rdistr_div_right False))) @@ \ |
|
180 \ (Try (Repeat (Rewrite rbinom_power_2 False))) @@ \ |
|
181 |
|
182 \ (Try (Repeat (Rewrite radd_commute False))) @@ \ |
|
183 \ (Try (Repeat (Rewrite radd_left_commute False))) @@ \ |
|
184 \ (Try (Repeat (Rewrite radd_assoc False))) @@ \ |
|
185 \ (Try (Repeat (Rewrite rmult_commute False))) @@ \ |
|
186 \ (Try (Repeat (Rewrite rmult_left_commute False))) @@ \ |
|
187 \ (Try (Repeat (Rewrite rmult_assoc False))) @@ \ |
|
188 |
|
189 \ (Try (Repeat (Rewrite radd_real_const_eq False))) @@ \ |
|
190 \ (Try (Repeat (Rewrite radd_real_const False))) @@ \ |
|
191 \ (Try (Repeat (Calculate plus))) @@ \ |
|
192 \ (Try (Repeat (Calculate times))) @@ \ |
|
193 \ (Try (Repeat (Calculate divide_))) @@\ |
|
194 \ (Try (Repeat (Calculate power_))) @@ \ |
|
195 |
|
196 \ (Try (Repeat (Rewrite rcollect_right False))) @@ \ |
|
197 \ (Try (Repeat (Rewrite rcollect_one_left False))) @@ \ |
|
198 \ (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ \ |
|
199 \ (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ \ |
|
200 |
|
201 \ (Try (Repeat (Rewrite rshift_nominator False))) @@ \ |
|
202 \ (Try (Repeat (Rewrite rcancel_den False))) @@ \ |
|
203 \ (Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
|
204 \ (Try (Repeat (Rewrite rroot_times_root False))) @@ \ |
|
205 \ (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ \ |
|
206 \ (Try (Repeat (Rewrite rsqare False))) @@ \ |
|
207 \ (Try (Repeat (Rewrite power_1 False))) @@ \ |
|
208 \ (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ \ |
|
209 \ (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ \ |
|
210 |
|
211 \ (Try (Repeat (Rewrite rmult_1 False))) @@ \ |
|
212 \ (Try (Repeat (Rewrite rmult_1_right False))) @@ \ |
|
213 \ (Try (Repeat (Rewrite rmult_0 False))) @@ \ |
|
214 \ (Try (Repeat (Rewrite rmult_0_right False))) @@ \ |
|
215 \ (Try (Repeat (Rewrite radd_0 False))) @@ \ |
|
216 \ (Try (Repeat (Rewrite radd_0_right False)))) \ |
|
217 \ t_)"; |
|
218 |
|
219 |
|
220 (* expects * distributed over + *) |
|
221 val Test_simplify = |
|
222 Rls{id = "Test_simplify", preconds = [], |
|
223 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), |
|
224 erls = tval_rls, srls = e_rls, |
|
225 calc=[(*since 040209 filled by prep_rls*)], |
|
226 (*asm_thm = [],*) |
|
227 rules = [ |
|
228 Thm ("real_diff_minus",num_str real_diff_minus), |
|
229 Thm ("radd_mult_distrib2",num_str radd_mult_distrib2), |
|
230 Thm ("rdistr_right_assoc",num_str rdistr_right_assoc), |
|
231 Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p), |
|
232 Thm ("rdistr_div_right",num_str rdistr_div_right), |
|
233 Thm ("rbinom_power_2",num_str rbinom_power_2), |
|
234 |
|
235 Thm ("radd_commute",num_str radd_commute), |
|
236 Thm ("radd_left_commute",num_str radd_left_commute), |
|
237 Thm ("radd_assoc",num_str radd_assoc), |
|
238 Thm ("rmult_commute",num_str rmult_commute), |
|
239 Thm ("rmult_left_commute",num_str rmult_left_commute), |
|
240 Thm ("rmult_assoc",num_str rmult_assoc), |
|
241 |
|
242 Thm ("radd_real_const_eq",num_str radd_real_const_eq), |
|
243 Thm ("radd_real_const",num_str radd_real_const), |
|
244 (* these 2 rules are invers to distr_div_right wrt. termination. |
|
245 thus they MUST be done IMMEDIATELY before calc *) |
|
246 Calc ("op +", eval_binop "#add_"), |
|
247 Calc ("op *", eval_binop "#mult_"), |
|
248 Calc ("HOL.divide", eval_cancel "#divide_"), |
|
249 Calc ("Atools.pow", eval_binop "#power_"), |
|
250 |
|
251 Thm ("rcollect_right",num_str rcollect_right), |
|
252 Thm ("rcollect_one_left",num_str rcollect_one_left), |
|
253 Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc), |
|
254 Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p), |
|
255 |
|
256 Thm ("rshift_nominator",num_str rshift_nominator), |
|
257 Thm ("rcancel_den",num_str rcancel_den), |
|
258 Thm ("rroot_square_inv",num_str rroot_square_inv), |
|
259 Thm ("rroot_times_root",num_str rroot_times_root), |
|
260 Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p), |
|
261 Thm ("rsqare",num_str rsqare), |
|
262 Thm ("power_1",num_str power_1), |
|
263 Thm ("rtwo_of_the_same",num_str rtwo_of_the_same), |
|
264 Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p), |
|
265 |
|
266 Thm ("rmult_1",num_str rmult_1), |
|
267 Thm ("rmult_1_right",num_str rmult_1_right), |
|
268 Thm ("rmult_0",num_str rmult_0), |
|
269 Thm ("rmult_0_right",num_str rmult_0_right), |
|
270 Thm ("radd_0",num_str radd_0), |
|
271 Thm ("radd_0_right",num_str radd_0_right) |
|
272 ], |
|
273 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
274 (*since 040209 filled by prep_rls: STest_simplify*) |
|
275 }:rls; |
|
276 |
|
277 |
|
278 |
|
279 |
|
280 |
|
281 (** rule sets **) |
|
282 |
|
283 |
|
284 |
|
285 (*isolate the root in a root-equation*) |
|
286 val isolate_root = |
|
287 Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), |
|
288 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *) |
|
289 rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs), |
|
290 Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult), |
|
291 Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult), |
|
292 Thm ("risolate_root_add",num_str risolate_root_add), |
|
293 Thm ("risolate_root_mult",num_str risolate_root_mult), |
|
294 Thm ("risolate_root_div",num_str risolate_root_div) ], |
|
295 scr = Script ((term_of o the o (parse thy)) |
|
296 "empty_script") |
|
297 }:rls; |
|
298 |
|
299 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
|
300 val isolate_bdv = |
|
301 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), |
|
302 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *) |
|
303 rules = |
|
304 [Thm ("risolate_bdv_add",num_str risolate_bdv_add), |
|
305 Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add), |
|
306 Thm ("risolate_bdv_mult",num_str risolate_bdv_mult), |
|
307 Thm ("mult_square",num_str mult_square), |
|
308 Thm ("constant_square",num_str constant_square), |
|
309 Thm ("constant_mult_square",num_str constant_mult_square) |
|
310 ], |
|
311 scr = Script ((term_of o the o (parse thy)) |
|
312 "empty_script") |
|
313 }:rls; |
|
314 |
|
315 |
|
316 |
|
317 |
|
318 (* association list for calculate_, calculate |
|
319 "op +" etc. not usable in scripts *) |
|
320 val calclist = |
|
321 [ |
|
322 (*as Tools.ML*) |
|
323 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")), |
|
324 ("matches",("Tools.matches",eval_matches "#matches_")), |
|
325 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
|
326 (*aus Atools.ML*) |
|
327 ("PLUS" ,("op +" ,eval_binop "#add_")), |
|
328 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
|
329 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
|
330 ("POWER" ,("Atools.pow" ,eval_binop "#power_")), |
|
331 ("is_const",("Atools.is'_const",eval_const "#is_const_")), |
|
332 ("le" ,("op <" ,eval_equ "#less_")), |
|
333 ("leq" ,("op <=" ,eval_equ "#less_equal_")), |
|
334 ("ident" ,("Atools.ident",eval_ident "#ident_")), |
|
335 (*von hier (ehem.SqRoot*) |
|
336 ("sqrt" ,("Root.sqrt" ,eval_sqrt "#sqrt_")), |
|
337 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")), |
|
338 ("Test.contains_root",("contains'_root", |
|
339 eval_contains_root"#contains_root_")) |
|
340 ]; |
|
341 |
|
342 ruleset' := overwritelthy thy (!ruleset', |
|
343 [("Test_simplify", prep_rls Test_simplify), |
|
344 ("tval_rls", prep_rls tval_rls), |
|
345 ("isolate_root", prep_rls isolate_root), |
|
346 ("isolate_bdv", prep_rls isolate_bdv), |
|
347 ("matches", |
|
348 prep_rls (append_rls "matches" testerls |
|
349 [Calc ("Tools.matches",eval_matches "#matches_")])) |
|
350 ]); |
|
351 |
|
352 (** problem types **) |
|
353 store_pbt |
|
354 (prep_pbt Test.thy "pbl_test" [] e_pblID |
|
355 (["test"], |
|
356 [], |
|
357 e_rls, NONE, [])); |
|
358 store_pbt |
|
359 (prep_pbt Test.thy "pbl_test_equ" [] e_pblID |
|
360 (["equation","test"], |
|
361 [("#Given" ,["equality e_","solveFor v_"]), |
|
362 ("#Where" ,["matches (?a = ?b) e_"]), |
|
363 ("#Find" ,["solutions v_i_"]) |
|
364 ], |
|
365 assoc_rls "matches", |
|
366 SOME "solve (e_::bool, v_)", [])); |
|
367 |
|
368 store_pbt |
|
369 (prep_pbt Test.thy "pbl_test_uni" [] e_pblID |
|
370 (["univariate","equation","test"], |
|
371 [("#Given" ,["equality e_","solveFor v_"]), |
|
372 ("#Where" ,["matches (?a = ?b) e_"]), |
|
373 ("#Find" ,["solutions v_i_"]) |
|
374 ], |
|
375 assoc_rls "matches", |
|
376 SOME "solve (e_::bool, v_)", [])); |
|
377 |
|
378 store_pbt |
|
379 (prep_pbt Test.thy "pbl_test_uni_lin" [] e_pblID |
|
380 (["linear","univariate","equation","test"], |
|
381 [("#Given" ,["equality e_","solveFor v_"]), |
|
382 ("#Where" ,["(matches ( v_ = 0) e_) | (matches ( ?b*v_ = 0) e_) |\ |
|
383 \(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_) "]), |
|
384 ("#Find" ,["solutions v_i_"]) |
|
385 ], |
|
386 assoc_rls "matches", |
|
387 SOME "solve (e_::bool, v_)", [["Test","solve_linear"]])); |
|
388 |
|
389 (*25.8.01 ------ |
|
390 store_pbt |
|
391 (prep_pbt Test.thy |
|
392 (["Test.thy"], |
|
393 [("#Given" ,"boolTestGiven g_"), |
|
394 ("#Find" ,"boolTestFind f_") |
|
395 ], |
|
396 [])); |
|
397 |
|
398 store_pbt |
|
399 (prep_pbt Test.thy |
|
400 (["testeq","Test.thy"], |
|
401 [("#Given" ,"boolTestGiven g_"), |
|
402 ("#Find" ,"boolTestFind f_") |
|
403 ], |
|
404 [])); |
|
405 |
|
406 |
|
407 val ttt = (term_of o the o (parse Isac.thy)) "(matches ( v_ = 0) e_)"; |
|
408 |
|
409 ------ 25.8.01*) |
|
410 |
|
411 |
|
412 (** methods **) |
|
413 store_met |
|
414 (prep_met Diff.thy "met_test" [] e_metID |
|
415 (["Test"], |
|
416 [], |
|
417 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
|
418 crls=Atools_erls, nrls=e_rls(*, |
|
419 asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
420 (* |
|
421 store_met |
|
422 (prep_met Script.thy |
|
423 (e_metID,(*empty method*) |
|
424 [], |
|
425 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], |
|
426 asm_rls=[],asm_thm=[]}, |
|
427 "Undef"));*) |
|
428 store_met |
|
429 (prep_met Test.thy "met_test_solvelin" [] e_metID |
|
430 (["Test","solve_linear"]:metID, |
|
431 [("#Given" ,["equality e_","solveFor v_"]), |
|
432 ("#Where" ,["matches (?a = ?b) e_"]), |
|
433 ("#Find" ,["solutions v_i_"]) |
|
434 ], |
|
435 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls, |
|
436 prls=assoc_rls "matches", |
|
437 calc=[], |
|
438 crls=tval_rls, nrls=Test_simplify}, |
|
439 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
440 \(let e_ =\ |
|
441 \ Repeat\ |
|
442 \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
443 \ (Rewrite_Set Test_simplify False))) e_\ |
|
444 \ in [e_::bool])" |
|
445 ) |
|
446 (*, prep_met Test.thy (*test for equations*) |
|
447 (["Test","testeq"]:metID, |
|
448 [("#Given" ,["boolTestGiven g_"]), |
|
449 ("#Find" ,["boolTestFind f_"]) |
|
450 ], |
|
451 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], |
|
452 asm_thm=[("square_equation_left","")]}, |
|
453 "Script Testeq (eq_::bool) = \ |
|
454 \Repeat \ |
|
455 \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_)); \ |
|
456 \ e_ = Try (Repeat (Rewrite square_equation_left True e_)); \ |
|
457 \ e_ = Try (Repeat (Rewrite rmult_0 False e_)) \ |
|
458 \ in e_) Until (is_root_free e_)" (*deleted*) |
|
459 ) |
|
460 , ---------27.4.02*) |
|
461 ); |
|
462 |
|
463 |
|
464 |
|
465 |
|
466 ruleset' := overwritelthy thy (!ruleset', |
|
467 [("norm_equation", prep_rls norm_equation), |
|
468 ("ac_plus_times", prep_rls ac_plus_times), |
|
469 ("rearrange_assoc", prep_rls rearrange_assoc) |
|
470 ]); |
|
471 |
|
472 |
|
473 fun bin_o (Const (op_,(Type ("fun", |
|
474 [Type (s2,[]),Type ("fun", |
|
475 [Type (s4,tl4),Type (s5,tl5)])])))) = |
|
476 if (s2=s4)andalso(s4=s5)then[op_]else[] |
|
477 | bin_o _ = []; |
|
478 |
|
479 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2) |
|
480 | bin_op t = bin_o t; |
|
481 fun is_bin_op t = ((bin_op t)<>[]); |
|
482 |
|
483 fun bin_op_arg1 ((Const (op_,(Type ("fun", |
|
484 [Type (s2,[]),Type ("fun", |
|
485 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = |
|
486 arg1; |
|
487 fun bin_op_arg2 ((Const (op_,(Type ("fun", |
|
488 [Type (s2,[]),Type ("fun", |
|
489 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = |
|
490 arg2; |
|
491 |
|
492 |
|
493 exception NO_EQUATION_TERM; |
|
494 fun is_equation ((Const ("op =",(Type ("fun", |
|
495 [Type (_,[]),Type ("fun", |
|
496 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _) |
|
497 = true |
|
498 | is_equation _ = false; |
|
499 fun equ_lhs ((Const ("op =",(Type ("fun", |
|
500 [Type (_,[]),Type ("fun", |
|
501 [Type (_,[]),Type ("bool",[])])])))) $ l $ r) |
|
502 = l |
|
503 | equ_lhs _ = raise NO_EQUATION_TERM; |
|
504 fun equ_rhs ((Const ("op =",(Type ("fun", |
|
505 [Type (_,[]),Type ("fun", |
|
506 [Type (_,[]),Type ("bool",[])])])))) $ l $ r) |
|
507 = r |
|
508 | equ_rhs _ = raise NO_EQUATION_TERM; |
|
509 |
|
510 |
|
511 fun atom (Const (_,Type (_,[]))) = true |
|
512 | atom (Free (_,Type (_,[]))) = true |
|
513 | atom (Var (_,Type (_,[]))) = true |
|
514 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *) |
|
515 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true |
|
516 | atom _ = false; |
|
517 |
|
518 fun varids (Const (s,Type (_,[]))) = [strip_thy s] |
|
519 | varids (Free (s,Type (_,[]))) = if is_no s then [] |
|
520 else [strip_thy s] |
|
521 | varids (Var((s,_),Type (_,[]))) = [strip_thy s] |
|
522 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *) |
|
523 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*) |
|
524 | varids (Abs(a,T,t)) = union op = [a] (varids t) |
|
525 | varids (t1 $ t2) = union op = (varids t1) (varids t2) |
|
526 | varids _ = []; |
|
527 (*> val t = term_of (hd (parse Diophant.thy "x")); |
|
528 val t = Free ("x","?DUMMY") : term |
|
529 > varids t; |
|
530 val it = [] : string list [] !!! *) |
|
531 |
|
532 |
|
533 fun bin_ops_only ((Const op_) $ t1 $ t2) = |
|
534 if(is_bin_op (Const op_)) |
|
535 then(bin_ops_only t1)andalso(bin_ops_only t2) |
|
536 else false |
|
537 | bin_ops_only t = |
|
538 if atom t then true else bin_ops_only t; |
|
539 |
|
540 fun polynomial opl t bdVar = (* bdVar TODO *) |
|
541 subset op = (bin_op t, opl) andalso (bin_ops_only t); |
|
542 |
|
543 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) |
|
544 andalso polynomial opl (equ_lhs t) bdVar |
|
545 andalso polynomial opl (equ_rhs t) bdVar |
|
546 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse |
|
547 subset op = (varids bdVar, varids (equ_lhs t))); |
|
548 |
|
549 (*fun max is = |
|
550 let fun max_ m [] = m |
|
551 | max_ m (i::is) = if m<i then max_ i is else max_ m is; |
|
552 in max_ (hd is) is end; |
|
553 > max [1,5,3,7,4,2]; |
|
554 val it = 7 : int *) |
|
555 |
|
556 fun max (a,b) = if a < b then b else a; |
|
557 |
|
558 fun degree addl mul bdVar t = |
|
559 let |
|
560 fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0 |
|
561 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0 |
|
562 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0 |
|
563 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *) |
|
564 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 |
|
565 | deg addl mul v (h $ t1 $ t2) = |
|
566 if subset op = (bin_op h, addl) |
|
567 then max (deg addl mul v t1 ,deg addl mul v t2) |
|
568 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2) |
|
569 in if polynomial (addl @ [mul]) t bdVar |
|
570 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option) |
|
571 end; |
|
572 fun degree_ addl mul bdVar t = (* do not export *) |
|
573 let fun opt (SOME i)= i |
|
574 | opt NONE = 0 |
|
575 in opt (degree addl mul bdVar t) end; |
|
576 |
|
577 |
|
578 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2; |
|
579 |
|
580 fun linear_equ addl mul bdVar t = |
|
581 if is_equation t |
|
582 then let val degl = degree_ addl mul bdVar (equ_lhs t); |
|
583 val degr = degree_ addl mul bdVar (equ_rhs t) |
|
584 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2 |
|
585 then true else false |
|
586 end |
|
587 else false; |
|
588 (* strip_thy op_ before *) |
|
589 fun is_div_op (dv,(Const (op_,(Type ("fun", |
|
590 [Type (s2,[]),Type ("fun", |
|
591 [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_) |
|
592 | is_div_op _ = false; |
|
593 |
|
594 fun is_denom bdVar div_op t = |
|
595 let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) |
|
596 | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) |
|
597 | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false) |
|
598 | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false |
|
599 | is bool[v]dv (h$n$d) = |
|
600 if is_div_op(dv,h) |
|
601 then (is false[v]dv n)orelse(is true[v]dv d) |
|
602 else (is bool [v]dv n)orelse(is bool[v]dv d) |
|
603 in is false (varids bdVar) (strip_thy div_op) t end; |
|
604 |
|
605 |
|
606 fun rational t div_op bdVar = |
|
607 is_denom bdVar div_op t andalso bin_ops_only t; |
|
608 |
|
609 |
|
610 |
|
611 (** problem types **) |
|
612 |
|
613 store_pbt |
|
614 (prep_pbt Test.thy "pbl_test_uni_plain2" [] e_pblID |
|
615 (["plain_square","univariate","equation","test"], |
|
616 [("#Given" ,["equality e_","solveFor v_"]), |
|
617 ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\ |
|
618 \(matches ( ?b*v_ ^^^2 = 0) e_) |\ |
|
619 \(matches (?a + v_ ^^^2 = 0) e_) |\ |
|
620 \(matches ( v_ ^^^2 = 0) e_)"]), |
|
621 ("#Find" ,["solutions v_i_"]) |
|
622 ], |
|
623 assoc_rls "matches", |
|
624 SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]])); |
|
625 (* |
|
626 val e_ = (term_of o the o (parse thy)) "e_::bool"; |
|
627 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0"; |
|
628 val env = [(e_,ve)]; |
|
629 |
|
630 val pre = (term_of o the o (parse thy)) |
|
631 "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |\ |
|
632 \(matches ( b*v_ ^^^2 = 0, e_::bool)) |\ |
|
633 \(matches (a + v_ ^^^2 = 0, e_::bool)) |\ |
|
634 \(matches ( v_ ^^^2 = 0, e_::bool))"; |
|
635 val prei = subst_atomic env pre; |
|
636 val cpre = (cterm_of thy) prei; |
|
637 |
|
638 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre; |
|
639 val ct = "True | False | False | False" : cterm |
|
640 |
|
641 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct; |
|
642 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct; |
|
643 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct; |
|
644 val ct = "True" : cterm |
|
645 |
|
646 *) |
|
647 |
|
648 store_pbt |
|
649 (prep_pbt Test.thy "pbl_test_uni_poly" [] e_pblID |
|
650 (["polynomial","univariate","equation","test"], |
|
651 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]), |
|
652 ("#Where" ,["False"]), |
|
653 ("#Find" ,["solutions v_i_"]) |
|
654 ], |
|
655 e_rls, SOME "solve (e_::bool, v_)", [])); |
|
656 |
|
657 store_pbt |
|
658 (prep_pbt Test.thy "pbl_test_uni_poly_deg2" [] e_pblID |
|
659 (["degree_two","polynomial","univariate","equation","test"], |
|
660 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]), |
|
661 ("#Find" ,["solutions v_i_"]) |
|
662 ], |
|
663 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", [])); |
|
664 |
|
665 store_pbt |
|
666 (prep_pbt Test.thy "pbl_test_uni_poly_deg2_pq" [] e_pblID |
|
667 (["pq_formula","degree_two","polynomial","univariate","equation","test"], |
|
668 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]), |
|
669 ("#Find" ,["solutions v_i_"]) |
|
670 ], |
|
671 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", [])); |
|
672 |
|
673 store_pbt |
|
674 (prep_pbt Test.thy "pbl_test_uni_poly_deg2_abc" [] e_pblID |
|
675 (["abc_formula","degree_two","polynomial","univariate","equation","test"], |
|
676 [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]), |
|
677 ("#Find" ,["solutions v_i_"]) |
|
678 ], |
|
679 e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", [])); |
|
680 |
|
681 store_pbt |
|
682 (prep_pbt Test.thy "pbl_test_uni_root" [] e_pblID |
|
683 (["squareroot","univariate","equation","test"], |
|
684 [("#Given" ,["equality e_","solveFor v_"]), |
|
685 ("#Where" ,["contains_root (e_::bool)"]), |
|
686 ("#Find" ,["solutions v_i_"]) |
|
687 ], |
|
688 append_rls "contains_root" e_rls [Calc ("Test.contains'_root", |
|
689 eval_contains_root "#contains_root_")], |
|
690 SOME "solve (e_::bool, v_)", [["Test","square_equation"]])); |
|
691 |
|
692 store_pbt |
|
693 (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID |
|
694 (["normalize","univariate","equation","test"], |
|
695 [("#Given" ,["equality e_","solveFor v_"]), |
|
696 ("#Where" ,[]), |
|
697 ("#Find" ,["solutions v_i_"]) |
|
698 ], |
|
699 e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]])); |
|
700 |
|
701 store_pbt |
|
702 (prep_pbt Test.thy "pbl_test_uni_roottest" [] e_pblID |
|
703 (["sqroot-test","univariate","equation","test"], |
|
704 [("#Given" ,["equality e_","solveFor v_"]), |
|
705 (*("#Where" ,["contains_root (e_::bool)"]),*) |
|
706 ("#Find" ,["solutions v_i_"]) |
|
707 ], |
|
708 e_rls, SOME "solve (e_::bool, v_)", [])); |
|
709 |
|
710 (* |
|
711 (#ppc o get_pbt) ["sqroot-test","univariate","equation"]; |
|
712 *) |
|
713 |
|
714 |
|
715 store_met |
|
716 (prep_met Test.thy "met_test_sqrt" [] e_metID |
|
717 (*root-equation, version for tests before 8.01.01*) |
|
718 (["Test","sqrt-equ-test"]:metID, |
|
719 [("#Given" ,["equality e_","solveFor v_"]), |
|
720 ("#Where" ,["contains_root (e_::bool)"]), |
|
721 ("#Find" ,["solutions v_i_"]) |
|
722 ], |
|
723 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
724 srls =append_rls "srls_contains_root" e_rls |
|
725 [Calc ("Test.contains'_root",eval_contains_root "")], |
|
726 prls =append_rls "prls_contains_root" e_rls |
|
727 [Calc ("Test.contains'_root",eval_contains_root "")], |
|
728 calc=[], |
|
729 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
730 asm_thm=[("square_equation_left",""), |
|
731 ("square_equation_right","")]*)}, |
|
732 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
733 \(let e_ = \ |
|
734 \ ((While (contains_root e_) Do\ |
|
735 \ ((Rewrite square_equation_left True) @@\ |
|
736 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
737 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
738 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
739 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
740 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
741 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
742 \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
743 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
744 \ e_\ |
|
745 \ in [e_::bool])" |
|
746 )); |
|
747 |
|
748 store_met |
|
749 (prep_met Test.thy "met_test_sqrt2" [] e_metID |
|
750 (*root-equation ... for test-*.sml until 8.01*) |
|
751 (["Test","squ-equ-test2"]:metID, |
|
752 [("#Given" ,["equality e_","solveFor v_"]), |
|
753 ("#Find" ,["solutions v_i_"]) |
|
754 ], |
|
755 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
756 srls = append_rls "srls_contains_root" e_rls |
|
757 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
758 prls=e_rls,calc=[], |
|
759 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
760 asm_thm=[("square_equation_left",""), |
|
761 ("square_equation_right","")]*)}, |
|
762 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
763 \(let e_ = \ |
|
764 \ ((While (contains_root e_) Do\ |
|
765 \ ((Rewrite square_equation_left True) @@\ |
|
766 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
767 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
768 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
769 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
770 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
771 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
772 \ (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
773 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
774 \ e_;\ |
|
775 \ (L_::bool list) = Tac subproblem_equation_dummy; \ |
|
776 \ L_ = Tac solve_equation_dummy \ |
|
777 \ in Check_elementwise L_ {(v_::real). Assumptions})" |
|
778 )); |
|
779 |
|
780 store_met |
|
781 (prep_met Test.thy "met_test_squ_sub" [] e_metID |
|
782 (*tests subproblem fixed linear*) |
|
783 (["Test","squ-equ-test-subpbl1"]:metID, |
|
784 [("#Given" ,["equality e_","solveFor v_"]), |
|
785 ("#Find" ,["solutions v_i_"]) |
|
786 ], |
|
787 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], |
|
788 crls=tval_rls, nrls=Test_simplify}, |
|
789 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
790 \ (let e_ = ((Try (Rewrite_Set norm_equation False)) @@ \ |
|
791 \ (Try (Rewrite_Set Test_simplify False))) e_; \ |
|
792 \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\ |
|
793 \ [Test,solve_linear]) [bool_ e_, real_ v_])\ |
|
794 \in Check_elementwise L_ {(v_::real). Assumptions})" |
|
795 )); |
|
796 |
|
797 store_met |
|
798 (prep_met Test.thy "met_test_squ_sub2" [] e_metID |
|
799 (*tests subproblem fixed degree 2*) |
|
800 (["Test","squ-equ-test-subpbl2"]:metID, |
|
801 [("#Given" ,["equality e_","solveFor v_"]), |
|
802 ("#Find" ,["solutions v_i_"]) |
|
803 ], |
|
804 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], |
|
805 crls=tval_rls, nrls=e_rls(*, |
|
806 asm_rls=[],asm_thm=[("square_equation_left",""), |
|
807 ("square_equation_right","")]*)}, |
|
808 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
809 \ (let e_ = Try (Rewrite_Set norm_equation False) e_; \ |
|
810 \(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\ |
|
811 \ [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])\ |
|
812 \in Check_elementwise L_ {(v_::real). Assumptions})" |
|
813 )); |
|
814 |
|
815 store_met |
|
816 (prep_met Test.thy "met_test_squ_nonterm" [] e_metID |
|
817 (*root-equation: see foils..., but notTerminating*) |
|
818 (["Test","square_equation...notTerminating"]:metID, |
|
819 [("#Given" ,["equality e_","solveFor v_"]), |
|
820 ("#Find" ,["solutions v_i_"]) |
|
821 ], |
|
822 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
823 srls = append_rls "srls_contains_root" e_rls |
|
824 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
825 prls=e_rls,calc=[], |
|
826 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
827 asm_thm=[("square_equation_left",""), |
|
828 ("square_equation_right","")]*)}, |
|
829 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
830 \(let e_ = \ |
|
831 \ ((While (contains_root e_) Do\ |
|
832 \ ((Rewrite square_equation_left True) @@\ |
|
833 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
834 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
835 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
836 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
837 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
838 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
839 \ e_;\ |
|
840 \ (L_::bool list) = \ |
|
841 \ (SubProblem (Test_,[linear,univariate,equation,test],\ |
|
842 \ [Test,solve_linear]) [bool_ e_, real_ v_])\ |
|
843 \in Check_elementwise L_ {(v_::real). Assumptions})" |
|
844 )); |
|
845 |
|
846 store_met |
|
847 (prep_met Test.thy "met_test_eq1" [] e_metID |
|
848 (*root-equation1:*) |
|
849 (["Test","square_equation1"]:metID, |
|
850 [("#Given" ,["equality e_","solveFor v_"]), |
|
851 ("#Find" ,["solutions v_i_"]) |
|
852 ], |
|
853 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
854 srls = append_rls "srls_contains_root" e_rls |
|
855 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
856 prls=e_rls,calc=[], |
|
857 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
858 asm_thm=[("square_equation_left",""), |
|
859 ("square_equation_right","")]*)}, |
|
860 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
861 \(let e_ = \ |
|
862 \ ((While (contains_root e_) Do\ |
|
863 \ ((Rewrite square_equation_left True) @@\ |
|
864 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
865 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
866 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
867 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
868 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
869 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
870 \ e_;\ |
|
871 \ (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test],\ |
|
872 \ [Test,solve_linear]) [bool_ e_, real_ v_])\ |
|
873 \ in Check_elementwise L_ {(v_::real). Assumptions})" |
|
874 )); |
|
875 |
|
876 store_met |
|
877 (prep_met Test.thy "met_test_squ2" [] e_metID |
|
878 (*root-equation2*) |
|
879 (["Test","square_equation2"]:metID, |
|
880 [("#Given" ,["equality e_","solveFor v_"]), |
|
881 ("#Find" ,["solutions v_i_"]) |
|
882 ], |
|
883 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
884 srls = append_rls "srls_contains_root" e_rls |
|
885 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
886 prls=e_rls,calc=[], |
|
887 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
888 asm_thm=[("square_equation_left",""), |
|
889 ("square_equation_right","")]*)}, |
|
890 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
891 \(let e_ = \ |
|
892 \ ((While (contains_root e_) Do\ |
|
893 \ (((Rewrite square_equation_left True) Or \ |
|
894 \ (Rewrite square_equation_right True)) @@\ |
|
895 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
896 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
897 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
898 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
899 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
900 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
901 \ e_;\ |
|
902 \ (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test],\ |
|
903 \ [Test,solve_plain_square]) [bool_ e_, real_ v_])\ |
|
904 \ in Check_elementwise L_ {(v_::real). Assumptions})" |
|
905 )); |
|
906 |
|
907 store_met |
|
908 (prep_met Test.thy "met_test_squeq" [] e_metID |
|
909 (*root-equation*) |
|
910 (["Test","square_equation"]:metID, |
|
911 [("#Given" ,["equality e_","solveFor v_"]), |
|
912 ("#Find" ,["solutions v_i_"]) |
|
913 ], |
|
914 {rew_ord'="e_rew_ord",rls'=tval_rls, |
|
915 srls = append_rls "srls_contains_root" e_rls |
|
916 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
917 prls=e_rls,calc=[], |
|
918 crls=tval_rls, nrls=e_rls(*,asm_rls=[], |
|
919 asm_thm=[("square_equation_left",""), |
|
920 ("square_equation_right","")]*)}, |
|
921 "Script Solve_root_equation (e_::bool) (v_::real) = \ |
|
922 \(let e_ = \ |
|
923 \ ((While (contains_root e_) Do\ |
|
924 \ (((Rewrite square_equation_left True) Or\ |
|
925 \ (Rewrite square_equation_right True)) @@\ |
|
926 \ (Try (Rewrite_Set Test_simplify False)) @@\ |
|
927 \ (Try (Rewrite_Set rearrange_assoc False)) @@\ |
|
928 \ (Try (Rewrite_Set isolate_root False)) @@\ |
|
929 \ (Try (Rewrite_Set Test_simplify False)))) @@\ |
|
930 \ (Try (Rewrite_Set norm_equation False)) @@\ |
|
931 \ (Try (Rewrite_Set Test_simplify False)))\ |
|
932 \ e_;\ |
|
933 \ (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\ |
|
934 \ [no_met]) [bool_ e_, real_ v_])\ |
|
935 \ in Check_elementwise L_ {(v_::real). Assumptions})" |
|
936 ) ); (*#######*) |
|
937 |
|
938 store_met |
|
939 (prep_met Test.thy "met_test_eq_plain" [] e_metID |
|
940 (*solve_plain_square*) |
|
941 (["Test","solve_plain_square"]:metID, |
|
942 [("#Given",["equality e_","solveFor v_"]), |
|
943 ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |\ |
|
944 \(matches ( ?b*v_ ^^^2 = 0) e_) |\ |
|
945 \(matches (?a + v_ ^^^2 = 0) e_) |\ |
|
946 \(matches ( v_ ^^^2 = 0) e_)"]), |
|
947 ("#Find" ,["solutions v_i_"]) |
|
948 ], |
|
949 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls, |
|
950 prls = assoc_rls "matches", |
|
951 crls=tval_rls, nrls=e_rls(*, |
|
952 asm_rls=[],asm_thm=[]*)}, |
|
953 "Script Solve_plain_square (e_::bool) (v_::real) = \ |
|
954 \ (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@ \ |
|
955 \ (Try (Rewrite_Set Test_simplify False)) @@ \ |
|
956 \ ((Rewrite square_equality_0 False) Or \ |
|
957 \ (Rewrite square_equality True)) @@ \ |
|
958 \ (Try (Rewrite_Set tval_rls False))) e_ \ |
|
959 \ in ((Or_to_List e_)::bool list))" |
|
960 )); |
|
961 |
|
962 store_met |
|
963 (prep_met Test.thy "met_test_norm_univ" [] e_metID |
|
964 (["Test","norm_univar_equation"]:metID, |
|
965 [("#Given",["equality e_","solveFor v_"]), |
|
966 ("#Where" ,[]), |
|
967 ("#Find" ,["solutions v_i_"]) |
|
968 ], |
|
969 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls, |
|
970 calc=[], |
|
971 crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)}, |
|
972 "Script Norm_univar_equation (e_::bool) (v_::real) = \ |
|
973 \ (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@ \ |
|
974 \ (Try (Rewrite_Set Test_simplify False))) e_ \ |
|
975 \ in (SubProblem (Test_,[univariate,equation,test], \ |
|
976 \ [no_met]) [bool_ e_, real_ v_]))" |
|
977 )); |
|
978 |
|
979 |
|
980 |
|
981 (*17.9.02 aus SqRoot.ML------------------------------^^^---*) |
|
982 |
|
983 (*8.4.03 aus Poly.ML--------------------------------vvv--- |
|
984 make_polynomial ---> make_poly |
|
985 ^-- for user ^-- for systest _ONLY_*) |
|
986 |
|
987 local (*. for make_polytest .*) |
|
988 |
|
989 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
990 |
|
991 fun pr_ord EQUAL = "EQUAL" |
|
992 | pr_ord LESS = "LESS" |
|
993 | pr_ord GREATER = "GREATER"; |
|
994 |
|
995 fun dest_hd' (Const (a, T)) = (* ~ term.ML *) |
|
996 (case a of |
|
997 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *) |
|
998 | _ => (((a, 0), T), 0)) |
|
999 | dest_hd' (Free (a, T)) = (((a, 0), T), 1) |
|
1000 | dest_hd' (Var v) = (v, 2) |
|
1001 | dest_hd' (Bound i) = ((("", i), dummyT), 3) |
|
1002 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); |
|
1003 (* RL *) |
|
1004 fun get_order_pow (t $ (Free(order,_))) = |
|
1005 (case int_of_str (order) of |
|
1006 SOME d => d |
|
1007 | NONE => 0) |
|
1008 | get_order_pow _ = 0; |
|
1009 |
|
1010 fun size_of_term' (Const(str,_) $ t) = |
|
1011 if "Atools.pow"= str then 1000 + size_of_term' t else 1 + size_of_term' t (*WN*) |
|
1012 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body |
|
1013 | size_of_term' (f$t) = size_of_term' f + size_of_term' t |
|
1014 | size_of_term' _ = 1; |
|
1015 |
|
1016 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) |
|
1017 (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord) |
|
1018 | term_ord' pr thy (t, u) = |
|
1019 (if pr then |
|
1020 let |
|
1021 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
|
1022 val _=writeln("t= f@ts= \""^ |
|
1023 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
|
1024 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\""); |
|
1025 val _=writeln("u= g@us= \""^ |
|
1026 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
|
1027 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\""); |
|
1028 val _=writeln("size_of_term(t,u)= ("^ |
|
1029 (string_of_int(size_of_term' t))^", "^ |
|
1030 (string_of_int(size_of_term' u))^")"); |
|
1031 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
|
1032 val _=writeln("terms_ord(ts,us) = "^ |
|
1033 ((pr_ord o terms_ord str false)(ts,us))); |
|
1034 val _=writeln("-------"); |
|
1035 in () end |
|
1036 else (); |
|
1037 case int_ord (size_of_term' t, size_of_term' u) of |
|
1038 EQUAL => |
|
1039 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in |
|
1040 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) |
|
1041 | ord => ord) |
|
1042 end |
|
1043 | ord => ord) |
|
1044 and hd_ord (f, g) = (* ~ term.ML *) |
|
1045 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g) |
|
1046 and terms_ord str pr (ts, us) = |
|
1047 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
|
1048 in |
|
1049 |
|
1050 fun ord_make_polytest (pr:bool) thy (_:subst) tu = |
|
1051 (term_ord' pr thy(***) tu = LESS ); |
|
1052 |
|
1053 end;(*local*) |
|
1054 |
|
1055 rew_ord' := overwritel (!rew_ord', |
|
1056 [("termlessI", termlessI), |
|
1057 ("ord_make_polytest", ord_make_polytest false thy) |
|
1058 ]); |
|
1059 |
|
1060 (*WN060510 this was a preparation for prep_rls ... |
|
1061 val scr_make_polytest = |
|
1062 "Script Expand_binomtest t_ =\ |
|
1063 \(Repeat \ |
|
1064 \((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
|
1065 |
|
1066 \ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \ |
|
1067 \ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \ |
|
1068 \ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \ |
|
1069 \ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \ |
|
1070 |
|
1071 \ (Try (Repeat (Rewrite real_mult_1 False))) @@ \ |
|
1072 \ (Try (Repeat (Rewrite real_mult_0 False))) @@ \ |
|
1073 \ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \ |
|
1074 |
|
1075 \ (Try (Repeat (Rewrite real_mult_commute False))) @@ \ |
|
1076 \ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \ |
|
1077 \ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \ |
|
1078 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
|
1079 \ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \ |
|
1080 \ (Try (Repeat (Rewrite real_add_assoc False))) @@ \ |
|
1081 |
|
1082 \ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \ |
|
1083 \ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \ |
|
1084 \ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \ |
|
1085 \ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \ |
|
1086 |
|
1087 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \ |
|
1088 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \ |
|
1089 |
|
1090 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \ |
|
1091 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \ |
|
1092 |
|
1093 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
1094 \ (Try (Repeat (Calculate times ))) @@ \ |
|
1095 \ (Try (Repeat (Calculate power_)))) \ |
|
1096 \ t_)"; |
|
1097 -----------------------------------------------------*) |
|
1098 |
|
1099 val make_polytest = |
|
1100 Rls{id = "make_polytest", preconds = []:term list, rew_ord = ("ord_make_polytest", |
|
1101 ord_make_polytest false Poly.thy), |
|
1102 erls = testerls, srls = Erls, |
|
1103 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
1104 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
1105 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
1106 ], |
|
1107 (*asm_thm = [],*) |
|
1108 rules = [Thm ("real_diff_minus",num_str real_diff_minus), |
|
1109 (*"a - b = a + (-1) * b"*) |
|
1110 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
1111 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
1112 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
1113 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
1114 Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib), |
|
1115 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
|
1116 Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2), |
|
1117 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
|
1118 Thm ("real_mult_1",num_str real_mult_1), |
|
1119 (*"1 * z = z"*) |
|
1120 Thm ("real_mult_0",num_str real_mult_0), |
|
1121 (*"0 * z = 0"*) |
|
1122 Thm ("real_add_zero_left",num_str real_add_zero_left), |
|
1123 (*"0 + z = z"*) |
|
1124 |
|
1125 (*AC-rewriting*) |
|
1126 Thm ("real_mult_commute",num_str real_mult_commute), |
|
1127 (* z * w = w * z *) |
|
1128 Thm ("real_mult_left_commute",num_str real_mult_left_commute), |
|
1129 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
|
1130 Thm ("real_mult_assoc",num_str real_mult_assoc), |
|
1131 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
|
1132 Thm ("real_add_commute",num_str real_add_commute), |
|
1133 (*z + w = w + z*) |
|
1134 Thm ("real_add_left_commute",num_str real_add_left_commute), |
|
1135 (*x + (y + z) = y + (x + z)*) |
|
1136 Thm ("real_add_assoc",num_str real_add_assoc), |
|
1137 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) |
|
1138 |
|
1139 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
1140 (*"r1 * r1 = r1 ^^^ 2"*) |
|
1141 Thm ("realpow_plus_1",num_str realpow_plus_1), |
|
1142 (*"r * r ^^^ n = r ^^^ (n + 1)"*) |
|
1143 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
1144 (*"z1 + z1 = 2 * z1"*) |
|
1145 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc), |
|
1146 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
1147 |
|
1148 Thm ("real_num_collect",num_str real_num_collect), |
|
1149 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
1150 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
1151 (*"[| l is_const; m is_const |] ==> |
|
1152 l * n + (m * n + k) = (l + m) * n + k"*) |
|
1153 Thm ("real_one_collect",num_str real_one_collect), |
|
1154 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
1155 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
1156 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
1157 |
|
1158 Calc ("op +", eval_binop "#add_"), |
|
1159 Calc ("op *", eval_binop "#mult_"), |
|
1160 Calc ("Atools.pow", eval_binop "#power_") |
|
1161 ], |
|
1162 scr = EmptyScr(*Script ((term_of o the o (parse thy)) |
|
1163 scr_make_polytest)*) |
|
1164 }:rls; |
|
1165 (*WN060510 this was done before 'fun prep_rls' ... |
|
1166 val scr_expand_binomtest = |
|
1167 "Script Expand_binomtest t_ =\ |
|
1168 \(Repeat \ |
|
1169 \((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \ |
|
1170 \ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \ |
|
1171 \ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \ |
|
1172 \ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \ |
|
1173 \ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \ |
|
1174 \ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \ |
|
1175 |
|
1176 \ (Try (Repeat (Rewrite real_mult_1 False))) @@ \ |
|
1177 \ (Try (Repeat (Rewrite real_mult_0 False))) @@ \ |
|
1178 \ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \ |
|
1179 |
|
1180 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
1181 \ (Try (Repeat (Calculate times ))) @@ \ |
|
1182 \ (Try (Repeat (Calculate power_))) @@ \ |
|
1183 |
|
1184 \ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \ |
|
1185 \ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \ |
|
1186 \ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \ |
|
1187 \ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \ |
|
1188 |
|
1189 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \ |
|
1190 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \ |
|
1191 |
|
1192 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \ |
|
1193 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \ |
|
1194 |
|
1195 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
1196 \ (Try (Repeat (Calculate times ))) @@ \ |
|
1197 \ (Try (Repeat (Calculate power_)))) \ |
|
1198 \ t_)"; |
|
1199 ------------------------------------------------------*) |
|
1200 |
|
1201 val expand_binomtest = |
|
1202 Rls{id = "expand_binomtest", preconds = [], |
|
1203 rew_ord = ("termlessI",termlessI), |
|
1204 erls = testerls, srls = Erls, |
|
1205 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
1206 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
1207 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
1208 ], |
|
1209 (*asm_thm = [],*) |
|
1210 rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2), |
|
1211 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) |
|
1212 Thm ("real_plus_binom_times" ,num_str real_plus_binom_times), |
|
1213 (*"(a + b)*(a + b) = ...*) |
|
1214 Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2), |
|
1215 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) |
|
1216 Thm ("real_minus_binom_times",num_str real_minus_binom_times), |
|
1217 (*"(a - b)*(a - b) = ...*) |
|
1218 Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1), |
|
1219 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) |
|
1220 Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2), |
|
1221 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) |
|
1222 (*RL 020915*) |
|
1223 Thm ("real_pp_binom_times",num_str real_pp_binom_times), |
|
1224 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
|
1225 Thm ("real_pm_binom_times",num_str real_pm_binom_times), |
|
1226 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) |
|
1227 Thm ("real_mp_binom_times",num_str real_mp_binom_times), |
|
1228 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) |
|
1229 Thm ("real_mm_binom_times",num_str real_mm_binom_times), |
|
1230 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) |
|
1231 Thm ("realpow_multI",num_str realpow_multI), |
|
1232 (*(a*b)^^^n = a^^^n * b^^^n*) |
|
1233 Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3), |
|
1234 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) |
|
1235 Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3), |
|
1236 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *) |
|
1237 |
|
1238 |
|
1239 (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
1240 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
1241 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
1242 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
1243 Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib), |
|
1244 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
|
1245 Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2), |
|
1246 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
|
1247 *) |
|
1248 |
|
1249 Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*) |
|
1250 Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*) |
|
1251 Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*) |
|
1252 |
|
1253 Calc ("op +", eval_binop "#add_"), |
|
1254 Calc ("op *", eval_binop "#mult_"), |
|
1255 Calc ("Atools.pow", eval_binop "#power_"), |
|
1256 (* |
|
1257 Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*) |
|
1258 Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**) |
|
1259 Thm ("real_mult_assoc",num_str real_mult_assoc), (**) |
|
1260 Thm ("real_add_commute",num_str real_add_commute), (**) |
|
1261 Thm ("real_add_left_commute",num_str real_add_left_commute), (**) |
|
1262 Thm ("real_add_assoc",num_str real_add_assoc), (**) |
|
1263 *) |
|
1264 |
|
1265 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
1266 (*"r1 * r1 = r1 ^^^ 2"*) |
|
1267 Thm ("realpow_plus_1",num_str realpow_plus_1), |
|
1268 (*"r * r ^^^ n = r ^^^ (n + 1)"*) |
|
1269 (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
1270 (*"z1 + z1 = 2 * z1"*)*) |
|
1271 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc), |
|
1272 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
1273 |
|
1274 Thm ("real_num_collect",num_str real_num_collect), |
|
1275 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) |
|
1276 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
1277 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
|
1278 Thm ("real_one_collect",num_str real_one_collect), |
|
1279 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
1280 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
1281 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
1282 |
|
1283 Calc ("op +", eval_binop "#add_"), |
|
1284 Calc ("op *", eval_binop "#mult_"), |
|
1285 Calc ("Atools.pow", eval_binop "#power_") |
|
1286 ], |
|
1287 scr = EmptyScr |
|
1288 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*) |
|
1289 }:rls; |
|
1290 |
|
1291 |
|
1292 ruleset' := overwritelthy thy (!ruleset', |
|
1293 [("make_polytest", prep_rls make_polytest), |
|
1294 ("expand_binomtest", prep_rls expand_binomtest) |
|
1295 ]); |
|
1296 |
|
1297 |
|
1298 |
|
1299 |
|
1300 |
|
1301 |