1 (* SML functions for rational arithmetic
3 use"../knowledge/Test.ML";
4 use"IsacKnowledge/Test.ML";
9 (** interface isabelle -- isac **)
11 theory' := overwritel (!theory', [("Test.thy",Test.thy)]);
13 (** evaluation of numerals and predicates **)
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 ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
22 Trueprop $ (mk_equality (t, false_as_term)))
23 else SOME (mk_thmid thmid ""
24 ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
25 Trueprop $ (mk_equality (t, true_as_term)))
26 | eval_root_free _ _ _ _ = NONE;
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 = "sqrt" (ids_of arg)
32 then SOME (mk_thmid thmid ""
33 ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
34 Trueprop $ (mk_equality (t, true_as_term)))
35 else SOME (mk_thmid thmid ""
36 ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
37 Trueprop $ (mk_equality (t, false_as_term)))
38 | eval_contains_root _ _ _ _ = NONE;
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_"))
48 fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
53 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
54 erls = e_rls, srls = Erls,
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),
68 Calc ("Atools.is'_const",eval_const "#is_const_"),
69 Calc ("Tools.matches",eval_matches ""),
71 Calc ("op +",eval_binop "#add_"),
72 Calc ("op *",eval_binop "#mult_"),
73 Calc ("Atools.pow" ,eval_binop "#power_"),
75 Calc ("op <",eval_equ "#less_"),
76 Calc ("op <=",eval_equ "#less_equal_"),
78 Calc ("Atools.ident",eval_ident "#ident_")],
79 scr = Script ((term_of o the o (parse thy))
83 (*.for evaluation of conditions in rewrite rules.*)
84 (*FIXXXXXXME 10.8.02: handle like _simplify*)
86 Rls{id = "tval_rls", preconds = [],
87 rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
88 erls=testerls,srls = e_rls,
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),
102 Thm ("real_diff_minus",num_str real_diff_minus),
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),
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_"),
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_"),
120 Calc ("op <",eval_equ "#less_"),
121 Calc ("op <=",eval_equ "#less_equal_"),
123 Calc ("Atools.ident",eval_ident "#ident_")],
124 scr = Script ((term_of o the o (parse thy))
129 ruleset' := overwritelthy thy (!ruleset',
130 [("testerls", prep_rls testerls)
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=[],*)
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))
147 Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
148 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
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))
160 (*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
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)
166 scr = Script ((term_of o the o (parse thy))
172 val STest_simplify = (* vv--- not changed to real by parse*)
173 "Script STest_simplify (t_::'z) = \
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))) @@ \
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))) @@ \
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_))) @@ \
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))) @@ \
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))) @@ \
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)))) \
220 (* expects * distributed over + *)
222 Rls{id = "Test_simplify", preconds = [],
223 rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
224 erls = tval_rls, srls = e_rls,
225 calc=[(*since 040209 filled by prep_rls*)],
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),
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),
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_"),
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),
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),
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)
273 scr = Script ((term_of o the o (parse thy)) "empty_script")
274 (*since 040209 filled by prep_rls: STest_simplify*)
285 (*isolate the root in a root-equation*)
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))
299 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
301 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
302 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
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)
311 scr = Script ((term_of o the o (parse thy))
318 (* association list for calculate_, calculate
319 "op +" etc. not usable in scripts *)
323 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
324 ("matches",("Tools.matches",eval_matches "#matches_")),
325 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
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_"))
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),
348 prep_rls (append_rls "matches" testerls
349 [Calc ("Tools.matches",eval_matches "#matches_")]))
352 (** problem types **)
354 (prep_pbt Test.thy "pbl_test" [] e_pblID
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_"])
366 SOME "solve (e_::bool, v_)", []));
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_"])
376 SOME "solve (e_::bool, v_)", []));
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_"])
387 SOME "solve (e_::bool, v_)", [["Test","solve_linear"]]));
393 [("#Given" ,"boolTestGiven g_"),
394 ("#Find" ,"boolTestFind f_")
400 (["testeq","Test.thy"],
401 [("#Given" ,"boolTestGiven g_"),
402 ("#Find" ,"boolTestFind f_")
407 val ttt = (term_of o the o (parse Isac.thy)) "(matches ( v_ = 0) e_)";
414 (prep_met Diff.thy "met_test" [] e_metID
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"));
423 (e_metID,(*empty method*)
425 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
426 asm_rls=[],asm_thm=[]},
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_"])
435 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
436 prls=assoc_rls "matches",
438 crls=tval_rls, nrls=Test_simplify},
439 "Script Solve_linear (e_::bool) (v_::real)= \
442 \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
443 \ (Rewrite_Set Test_simplify False))) e_\
446 (*, prep_met Test.thy (*test for equations*)
447 (["Test","testeq"]:metID,
448 [("#Given" ,["boolTestGiven g_"]),
449 ("#Find" ,["boolTestFind f_"])
451 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
452 asm_thm=[("square_equation_left","")]},
453 "Script Testeq (eq_::bool) = \
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*)
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)
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[]
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)<>[]);
483 fun bin_op_arg1 ((Const (op_,(Type ("fun",
484 [Type (s2,[]),Type ("fun",
485 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
487 fun bin_op_arg2 ((Const (op_,(Type ("fun",
488 [Type (s2,[]),Type ("fun",
489 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
493 exception NO_EQUATION_TERM;
494 fun is_equation ((Const ("op =",(Type ("fun",
495 [Type (_,[]),Type ("fun",
496 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
498 | is_equation _ = false;
499 fun equ_lhs ((Const ("op =",(Type ("fun",
500 [Type (_,[]),Type ("fun",
501 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
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)
508 | equ_rhs _ = raise NO_EQUATION_TERM;
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
518 fun varids (Const (s,Type (_,[]))) = [strip_thy s]
519 | varids (Free (s,Type (_,[]))) = if is_no s then []
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)
527 (*> val t = term_of (hd (parse Diophant.thy "x"));
528 val t = Free ("x","?DUMMY") : term
530 val it = [] : string list [] !!! *)
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)
538 if atom t then true else bin_ops_only t;
540 fun polynomial opl t bdVar = (* bdVar TODO *)
541 subset op = (bin_op t, opl) andalso (bin_ops_only t);
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)));
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;
556 fun max (a,b) = if a < b then b else a;
558 fun degree addl mul bdVar t =
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)
572 fun degree_ addl mul bdVar t = (* do not export *)
573 let fun opt (SOME i)= i
575 in opt (degree addl mul bdVar t) end;
578 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
580 fun linear_equ addl mul bdVar 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
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;
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) =
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;
606 fun rational t div_op bdVar =
607 is_denom bdVar div_op t andalso bin_ops_only t;
611 (** problem types **)
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_"])
624 SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));
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";
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 (sign_of thy) prei;
638 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
639 val ct = "True | False | False | False" : cterm
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
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_"])
655 e_rls, SOME "solve (e_::bool, v_)", []));
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_"])
663 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
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_"])
671 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
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_"])
679 e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));
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_"])
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"]]));
693 (prep_pbt Test.thy "pbl_test_uni_norm" [] e_pblID
694 (["normalize","univariate","equation","test"],
695 [("#Given" ,["equality e_","solveFor v_"]),
697 ("#Find" ,["solutions v_i_"])
699 e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));
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_"])
708 e_rls, SOME "solve (e_::bool, v_)", []));
711 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
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_"])
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 "")],
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) = \
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)))\
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_"])
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"")],
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) = \
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)))\
775 \ (L_::bool list) = Tac subproblem_equation_dummy; \
776 \ L_ = Tac solve_equation_dummy \
777 \ in Check_elementwise L_ {(v_::real). Assumptions})"
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_"])
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})"
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_"])
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})"
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_"])
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"")],
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) = \
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)))\
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})"
847 (prep_met Test.thy "met_test_eq1" [] e_metID
849 (["Test","square_equation1"]:metID,
850 [("#Given" ,["equality e_","solveFor v_"]),
851 ("#Find" ,["solutions v_i_"])
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"")],
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) = \
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)))\
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})"
877 (prep_met Test.thy "met_test_squ2" [] e_metID
879 (["Test","square_equation2"]:metID,
880 [("#Given" ,["equality e_","solveFor v_"]),
881 ("#Find" ,["solutions v_i_"])
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"")],
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) = \
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)))\
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})"
908 (prep_met Test.thy "met_test_squeq" [] e_metID
910 (["Test","square_equation"]:metID,
911 [("#Given" ,["equality e_","solveFor v_"]),
912 ("#Find" ,["solutions v_i_"])
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"")],
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) = \
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)))\
933 \ (L_::bool list) = (SubProblem (Test_,[univariate,equation,test],\
934 \ [no_met]) [bool_ e_, real_ v_])\
935 \ in Check_elementwise L_ {(v_::real). Assumptions})"
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_"])
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))"
963 (prep_met Test.thy "met_test_norm_univ" [] e_metID
964 (["Test","norm_univar_equation"]:metID,
965 [("#Given",["equality e_","solveFor v_"]),
967 ("#Find" ,["solutions v_i_"])
969 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
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_]))"
981 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
983 (*8.4.03 aus Poly.ML--------------------------------vvv---
984 make_polynomial ---> make_poly
985 ^-- for user ^-- for systest _ONLY_*)
987 local (*. for make_polytest .*)
989 open Term; (* for type order = EQUAL | LESS | GREATER *)
991 fun pr_ord EQUAL = "EQUAL"
992 | pr_ord LESS = "LESS"
993 | pr_ord GREATER = "GREATER";
995 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
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);
1004 fun get_order_pow (t $ (Free(order,_))) =
1005 (case int_of_str (order) of
1008 | get_order_pow _ = 0;
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;
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) =
1021 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1022 val _=writeln("t= f@ts= \""^
1023 ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
1024 (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
1025 val _=writeln("u= g@us= \""^
1026 ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
1027 (commas(map(string_of_cterm o cterm_of (sign_of 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("-------");
1037 case int_ord (size_of_term' t, size_of_term' u) of
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)
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);
1050 fun ord_make_polytest (pr:bool) thy (_:subst) tu =
1051 (term_ord' pr thy(***) tu = LESS );
1055 rew_ord' := overwritel (!rew_ord',
1056 [("termlessI", termlessI),
1057 ("ord_make_polytest", ord_make_polytest false thy)
1060 (*WN060510 this was a preparation for prep_rls ...
1061 val scr_make_polytest =
1062 "Script Expand_binomtest t_ =\
1064 \((Try (Repeat (Rewrite real_diff_minus False))) @@ \
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))) @@ \
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))) @@ \
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))) @@ \
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))) @@ \
1087 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1088 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1090 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1091 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1093 \ (Try (Repeat (Calculate plus ))) @@ \
1094 \ (Try (Repeat (Calculate times ))) @@ \
1095 \ (Try (Repeat (Calculate power_)))) \
1097 -----------------------------------------------------*)
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_"))
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),
1120 Thm ("real_mult_0",num_str real_mult_0),
1122 Thm ("real_add_zero_left",num_str real_add_zero_left),
1126 Thm ("real_mult_commute",num_str real_mult_commute),
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),
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)*)
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"*)
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"*)
1158 Calc ("op +", eval_binop "#add_"),
1159 Calc ("op *", eval_binop "#mult_"),
1160 Calc ("Atools.pow", eval_binop "#power_")
1162 scr = EmptyScr(*Script ((term_of o the o (parse thy))
1163 scr_make_polytest)*)
1165 (*WN060510 this was done before 'fun prep_rls' ...
1166 val scr_expand_binomtest =
1167 "Script Expand_binomtest t_ =\
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))) @@ \
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))) @@ \
1180 \ (Try (Repeat (Calculate plus ))) @@ \
1181 \ (Try (Repeat (Calculate times ))) @@ \
1182 \ (Try (Repeat (Calculate power_))) @@ \
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))) @@ \
1189 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1190 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1192 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1193 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1195 \ (Try (Repeat (Calculate plus ))) @@ \
1196 \ (Try (Repeat (Calculate times ))) @@ \
1197 \ (Try (Repeat (Calculate power_)))) \
1199 ------------------------------------------------------*)
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_"))
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"*)
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 *)
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"*)
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"*)
1253 Calc ("op +", eval_binop "#add_"),
1254 Calc ("op *", eval_binop "#mult_"),
1255 Calc ("Atools.pow", eval_binop "#power_"),
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), (**)
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"*)
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"*)
1283 Calc ("op +", eval_binop "#add_"),
1284 Calc ("op *", eval_binop "#mult_"),
1285 Calc ("Atools.pow", eval_binop "#power_")
1288 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
1292 ruleset' := overwritelthy thy (!ruleset',
1293 [("make_polytest", prep_rls make_polytest),
1294 ("expand_binomtest", prep_rls expand_binomtest)