1 (* some tests are based on specficially simple scripts etc.
2 Author: Walther Neuper 2003
3 (c) due to copyright terms
6 theory Test imports Atools Poly Rational Root Diff begin
10 (*"cancel":: [real, real] => real (infixl "'/'/'/" 70) ...divide 2002*)
15 ("((Script Expand'_binomtest (_ =))//
20 bool list] => bool list"
21 ("((Script Solve'_univar'_err (_ _ _ =))//
26 bool list] => bool list"
27 ("((Script Solve'_linear (_ _ =))//
30 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
32 "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
33 "contains'_root" :: "'a => bool" ("contains'_root _" 10)
37 bool list] => bool list"
38 ("((Script Solve'_root'_equation (_ _ =))//
43 bool list] => bool list"
44 ("((Script Solve'_plain'_square (_ _ =))//
47 Norm'_univar'_equation
50 ("((Script Norm'_univar'_equation (_ _ =))//
56 ("((Script STest'_simplify (_ =))//
59 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
61 axioms (*TODO: prove as theorems*)
63 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n"
64 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n"
65 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k"
66 rdistr_div_right: "((k::real) + l) / n = k / n + l / n"
68 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
70 "m is_const ==> (n::real) + m * n = (1 + m) * n"
71 rcollect_one_left_assoc:
72 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
73 rcollect_one_left_assoc_p:
74 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
76 rtwo_of_the_same: "a + a = 2 * a"
77 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a"
78 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x"
80 rcancel_den: "not(a=0) ==> a * (b / a) = b"
81 rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
82 rshift_nominator: "(a::real) * b / c = a / c * b"
84 exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
85 rsqare: "(a::real) * a = a ^^^ 2"
86 power_1: "(a::real) ^^^ 1 = a"
87 rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
89 rmult_1: "1 * k = (k::real)"
90 rmult_1_right: "k * 1 = (k::real)"
91 rmult_0: "0 * k = (0::real)"
92 rmult_0_right: "k * 0 = (0::real)"
93 radd_0: "0 + k = (k::real)"
94 radd_0_right: "k + 0 = (k::real)"
97 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
99 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
102 radd_commute: "(m::real) + (n::real) = n + m"
103 radd_left_commute: "(x::real) + (y + z) = y + (x + z)"
104 radd_assoc: "(m::real) + n + k = m + (n + k)"
105 rmult_commute: "(m::real) * n = n * m"
106 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)"
107 rmult_assoc: "(m::real) * n * k = m * (n * k)"
109 (*for equations: 'bdv' is a meta-constant*)
110 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
111 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
112 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)"
115 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
117 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
118 root_ge0: "0 <= a ==> 0 <= sqrt a"
119 (*should be dropped with better simplification in eval_rls ...*)
121 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
125 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
128 rroot_square_inv: "(sqrt a)^^^ 2 = a"
129 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)"
130 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
131 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
134 (*for root-equations*)
135 square_equation_left:
136 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
137 square_equation_right:
138 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
139 (*causes frequently non-termination:*)
141 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
143 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
144 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
145 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)"
147 (*for polynomial equations of degree 2; linear case in RatArith*)
148 mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
149 constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
150 constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
153 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
155 "(x^^^2 = 0) = (x = 0)"
157 (*isolate root on the LEFT hand side of the equation
158 otherwise shuffling from left to right would not terminate*)
161 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
163 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
164 rroot_to_lhs_add_mult:
165 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
171 (** evaluation of numerals and predicates **)
173 (*does a term contain a root ?*)
174 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =
175 if strip_thy op0 <> "is'_root'_free"
176 then error ("eval_root_free: wrong "^op0)
177 else if const_in (strip_thy op0) arg
178 then SOME (mk_thmid thmid ""
179 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
180 Trueprop $ (mk_equality (t, false_as_term)))
181 else SOME (mk_thmid thmid ""
182 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
183 Trueprop $ (mk_equality (t, true_as_term)))
184 | eval_root_free _ _ _ _ = NONE;
186 (*does a term contain a root ?*)
187 fun eval_contains_root (thmid:string) _
188 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
189 if member op = (ids_of arg) "sqrt"
190 then SOME (mk_thmid thmid ""
191 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
192 Trueprop $ (mk_equality (t, true_as_term)))
193 else SOME (mk_thmid thmid ""
194 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
195 Trueprop $ (mk_equality (t, false_as_term)))
196 | eval_contains_root _ _ _ _ = NONE;
198 calclist':= overwritel (!calclist',
199 [("is_root_free", ("Test.is'_root'_free",
200 eval_root_free"#is_root_free_e")),
201 ("contains_root", ("Test.contains'_root",
202 eval_contains_root"#contains_root_"))
206 fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
212 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
213 erls = e_rls, srls = Erls,
215 rules = [Thm ("refl",num_str @{thm refl}),
216 Thm ("real_le_refl",num_str @{thm real_le_refl}),
217 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
218 Thm ("not_true",num_str @{thm not_true}),
219 Thm ("not_false",num_str @{thm not_false}),
220 Thm ("and_true",num_str @{thm and_true}),
221 Thm ("and_false",num_str @{thm and_false}),
222 Thm ("or_true",num_str @{thm or_true}),
223 Thm ("or_false",num_str @{thm or_false}),
224 Thm ("and_commute",num_str @{thm and_commute}),
225 Thm ("or_commute",num_str @{thm or_commute}),
227 Calc ("Atools.is'_const",eval_const "#is_const_"),
228 Calc ("Tools.matches",eval_matches ""),
230 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
231 Calc ("op *",eval_binop "#mult_"),
232 Calc ("Atools.pow" ,eval_binop "#power_"),
234 Calc ("op <",eval_equ "#less_"),
235 Calc ("op <=",eval_equ "#less_equal_"),
237 Calc ("Atools.ident",eval_ident "#ident_")],
238 scr = Script ((term_of o the o (parse thy))
243 (*.for evaluation of conditions in rewrite rules.*)
244 (*FIXXXXXXME 10.8.02: handle like _simplify*)
246 Rls{id = "tval_rls", preconds = [],
247 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
248 erls=testerls,srls = e_rls,
250 rules = [Thm ("refl",num_str @{thm refl}),
251 Thm ("real_le_refl",num_str @{thm real_le_refl}),
252 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
253 Thm ("not_true",num_str @{thm not_true}),
254 Thm ("not_false",num_str @{thm not_false}),
255 Thm ("and_true",num_str @{thm and_true}),
256 Thm ("and_false",num_str @{thm and_false}),
257 Thm ("or_true",num_str @{thm or_true}),
258 Thm ("or_false",num_str @{thm or_false}),
259 Thm ("and_commute",num_str @{thm and_commute}),
260 Thm ("or_commute",num_str @{thm or_commute}),
262 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
264 Thm ("root_ge0",num_str @{thm root_ge0}),
265 Thm ("root_add_ge0",num_str @{thm root_add_ge0}),
266 Thm ("root_ge0_1",num_str @{thm root_ge0_1}),
267 Thm ("root_ge0_2",num_str @{thm root_ge0_2}),
269 Calc ("Atools.is'_const",eval_const "#is_const_"),
270 Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_e"),
271 Calc ("Tools.matches",eval_matches ""),
272 Calc ("Test.contains'_root",
273 eval_contains_root"#contains_root_"),
275 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
276 Calc ("op *",eval_binop "#mult_"),
277 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
278 Calc ("Atools.pow" ,eval_binop "#power_"),
280 Calc ("op <",eval_equ "#less_"),
281 Calc ("op <=",eval_equ "#less_equal_"),
283 Calc ("Atools.ident",eval_ident "#ident_")],
284 scr = Script ((term_of o the o (parse thy))
290 ruleset' := overwritelthy @{theory} (!ruleset',
291 [("testerls", prep_rls testerls)
295 (*make () dissappear*)
296 val rearrange_assoc =
297 Rls{id = "rearrange_assoc", preconds = [],
298 rew_ord = ("e_rew_ord",e_rew_ord),
299 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
301 [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
302 Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
303 scr = Script ((term_of o the o (parse thy))
308 Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
309 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
311 [Thm ("radd_commute",num_str @{thm radd_commute}),
312 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
313 Thm ("add_assoc",num_str @{thm add_assoc}),
314 Thm ("rmult_commute",num_str @{thm rmult_commute}),
315 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
316 Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
317 scr = Script ((term_of o the o (parse thy))
321 (*todo: replace by Rewrite("rnorm_equation_add",num_str @{thm rnorm_equation_add)*)
323 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
324 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
325 rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
327 scr = Script ((term_of o the o (parse thy))
334 val STest_simplify = (* vv--- not changed to real by parse*)
335 "Script STest_simplify (t_t::'z) = " ^
337 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
338 " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
339 " (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ " ^
340 " (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^
341 " (Try (Repeat (Rewrite rdistr_div_right False))) @@ " ^
342 " (Try (Repeat (Rewrite rbinom_power_2 False))) @@ " ^
344 " (Try (Repeat (Rewrite radd_commute False))) @@ " ^
345 " (Try (Repeat (Rewrite radd_left_commute False))) @@ " ^
346 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
347 " (Try (Repeat (Rewrite rmult_commute False))) @@ " ^
348 " (Try (Repeat (Rewrite rmult_left_commute False))) @@ " ^
349 " (Try (Repeat (Rewrite rmult_assoc False))) @@ " ^
351 " (Try (Repeat (Rewrite radd_real_const_eq False))) @@ " ^
352 " (Try (Repeat (Rewrite radd_real_const False))) @@ " ^
353 " (Try (Repeat (Calculate PLUS))) @@ " ^
354 " (Try (Repeat (Calculate TIMES))) @@ " ^
355 " (Try (Repeat (Calculate divide_))) @@" ^
356 " (Try (Repeat (Calculate POWER))) @@ " ^
358 " (Try (Repeat (Rewrite rcollect_right False))) @@ " ^
359 " (Try (Repeat (Rewrite rcollect_one_left False))) @@ " ^
360 " (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ " ^
361 " (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ " ^
363 " (Try (Repeat (Rewrite rshift_nominator False))) @@ " ^
364 " (Try (Repeat (Rewrite rcancel_den False))) @@ " ^
365 " (Try (Repeat (Rewrite rroot_square_inv False))) @@ " ^
366 " (Try (Repeat (Rewrite rroot_times_root False))) @@ " ^
367 " (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ " ^
368 " (Try (Repeat (Rewrite rsqare False))) @@ " ^
369 " (Try (Repeat (Rewrite power_1 False))) @@ " ^
370 " (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ " ^
371 " (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ " ^
373 " (Try (Repeat (Rewrite rmult_1 False))) @@ " ^
374 " (Try (Repeat (Rewrite rmult_1_right False))) @@ " ^
375 " (Try (Repeat (Rewrite rmult_0 False))) @@ " ^
376 " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
377 " (Try (Repeat (Rewrite radd_0 False))) @@ " ^
378 " (Try (Repeat (Rewrite radd_0_right False)))) " ^
383 (* expects * distributed over + *)
385 Rls{id = "Test_simplify", preconds = [],
386 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
387 erls = tval_rls, srls = e_rls,
388 calc=[(*since 040209 filled by prep_rls*)],
391 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
392 Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}),
393 Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}),
394 Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}),
395 Thm ("rdistr_div_right",num_str @{thm rdistr_div_right}),
396 Thm ("rbinom_power_2",num_str @{thm rbinom_power_2}),
398 Thm ("radd_commute",num_str @{thm radd_commute}),
399 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
400 Thm ("add_assoc",num_str @{thm add_assoc}),
401 Thm ("rmult_commute",num_str @{thm rmult_commute}),
402 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
403 Thm ("rmult_assoc",num_str @{thm rmult_assoc}),
405 Thm ("radd_real_const_eq",num_str @{thm radd_real_const_eq}),
406 Thm ("radd_real_const",num_str @{thm radd_real_const}),
407 (* these 2 rules are invers to distr_div_right wrt. termination.
408 thus they MUST be done IMMEDIATELY before calc *)
409 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
410 Calc ("op *", eval_binop "#mult_"),
411 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
412 Calc ("Atools.pow", eval_binop "#power_"),
414 Thm ("rcollect_right",num_str @{thm rcollect_right}),
415 Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}),
416 Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}),
417 Thm ("rcollect_one_left_assoc_p",num_str @{thm rcollect_one_left_assoc_p}),
419 Thm ("rshift_nominator",num_str @{thm rshift_nominator}),
420 Thm ("rcancel_den",num_str @{thm rcancel_den}),
421 Thm ("rroot_square_inv",num_str @{thm rroot_square_inv}),
422 Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
423 Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
424 Thm ("rsqare",num_str @{thm rsqare}),
425 Thm ("power_1",num_str @{thm power_1}),
426 Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
427 Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
429 Thm ("rmult_1",num_str @{thm rmult_1}),
430 Thm ("rmult_1_right",num_str @{thm rmult_1_right}),
431 Thm ("rmult_0",num_str @{thm rmult_0}),
432 Thm ("rmult_0_right",num_str @{thm rmult_0_right}),
433 Thm ("radd_0",num_str @{thm radd_0}),
434 Thm ("radd_0_right",num_str @{thm radd_0_right})
436 scr = Script ((term_of o the o (parse thy)) "empty_script")
437 (*since 040209 filled by prep_rls: STest_simplify*)
446 (*isolate the root in a root-equation*)
448 Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
449 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
450 rules = [Thm ("rroot_to_lhs",num_str @{thm rroot_to_lhs}),
451 Thm ("rroot_to_lhs_mult",num_str @{thm rroot_to_lhs_mult}),
452 Thm ("rroot_to_lhs_add_mult",num_str @{thm rroot_to_lhs_add_mult}),
453 Thm ("risolate_root_add",num_str @{thm risolate_root_add}),
454 Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),
455 Thm ("risolate_root_div",num_str @{thm risolate_root_div}) ],
456 scr = Script ((term_of o the o (parse thy))
460 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
462 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
463 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
465 [Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
466 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
467 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
468 Thm ("mult_square",num_str @{thm mult_square}),
469 Thm ("constant_square",num_str @{thm constant_square}),
470 Thm ("constant_mult_square",num_str @{thm constant_mult_square})
472 scr = Script ((term_of o the o (parse thy))
478 (* association list for calculate_, calculate
479 "Groups.plus_class.plus" etc. not usable in scripts *)
483 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
484 ("matches",("Tools.matches",eval_matches "#matches_")),
485 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
487 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
488 ("TIMES" ,("op *" ,eval_binop "#mult_")),
489 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
490 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
491 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
492 ("le" ,("op <" ,eval_equ "#less_")),
493 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
494 ("ident" ,("Atools.ident",eval_ident "#ident_")),
495 (*von hier (ehem.SqRoot*)
496 ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
497 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),
498 ("Test.contains_root",("contains'_root",
499 eval_contains_root"#contains_root_"))
502 ruleset' := overwritelthy @{theory} (!ruleset',
503 [("Test_simplify", prep_rls Test_simplify),
504 ("tval_rls", prep_rls tval_rls),
505 ("isolate_root", prep_rls isolate_root),
506 ("isolate_bdv", prep_rls isolate_bdv),
508 prep_rls (append_rls "matches" testerls
509 [Calc ("Tools.matches",eval_matches "#matches_")]))
514 (** problem types **)
516 (prep_pbt thy "pbl_test" [] e_pblID
521 (prep_pbt thy "pbl_test_equ" [] e_pblID
522 (["equation","test"],
523 [("#Given" ,["equality e_e","solveFor v_v"]),
524 ("#Where" ,["matches (?a = ?b) e_e"]),
525 ("#Find" ,["solutions v_v'i'"])
528 SOME "solve (e_e::bool, v_v)", []));
531 (prep_pbt thy "pbl_test_uni" [] e_pblID
532 (["univariate","equation","test"],
533 [("#Given" ,["equality e_e","solveFor v_v"]),
534 ("#Where" ,["matches (?a = ?b) e_e"]),
535 ("#Find" ,["solutions v_v'i'"])
538 SOME "solve (e_e::bool, v_v)", []));
541 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
542 (["linear","univariate","equation","test"],
543 [("#Given" ,["equality e_e","solveFor v_v"]),
544 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
545 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
546 ("#Find" ,["solutions v_v'i'"])
549 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
555 [("#Given" ,"boolTestGiven g_g"),
556 ("#Find" ,"boolTestFind f_f")
563 [("#Given" ,"boolTestGiven g_g"),
564 ("#Find" ,"boolTestFind f_f")
569 val ttt = (term_of o the o (parse (theory "Isac"))) "(matches ( v_v = 0) e_e)";
577 (prep_met (theory "Diff") "met_test" [] e_metID
580 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
581 crls=Atools_erls, nrls=e_rls(*,
582 asm_rls=[],asm_thm=[]*)}, "empty_script"));
585 (prep_met (theory "Script")
586 (e_metID,(*empty method*)
588 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
589 asm_rls=[],asm_thm=[]},
594 (prep_met thy "met_test_solvelin" [] e_metID
595 (["Test","solve_linear"]:metID,
596 [("#Given" ,["equality e_e","solveFor v_v"]),
597 ("#Where" ,["matches (?a = ?b) e_e"]),
598 ("#Find" ,["solutions v_v'i'"])
600 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
601 prls = assoc_rls "matches", calc = [], crls = tval_rls,
602 nrls = Test_simplify},
603 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
606 " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
607 " (Rewrite_Set Test_simplify False))) e_e" ^
610 (*, prep_met thy (*test for equations*)
611 (["Test","testeq"]:metID,
612 [("#Given" ,["boolTestGiven g_g"]),
613 ("#Find" ,["boolTestFind f_f"])
615 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
616 asm_thm=[("square_equation_left","")]},
617 "Script Testeq (e_q::bool) = " ^
619 " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
620 " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
621 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
622 " in e_e) Until (is_root_free e_e)" (*deleted*)
630 ruleset' := overwritelthy @{theory} (!ruleset',
631 [("norm_equation", prep_rls norm_equation),
632 ("ac_plus_times", prep_rls ac_plus_times),
633 ("rearrange_assoc", prep_rls rearrange_assoc)
637 fun bin_o (Const (op_,(Type ("fun",
638 [Type (s2,[]),Type ("fun",
639 [Type (s4,tl4),Type (s5,tl5)])])))) =
640 if (s2=s4)andalso(s4=s5)then[op_]else[]
643 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
644 | bin_op t = bin_o t;
645 fun is_bin_op t = ((bin_op t)<>[]);
647 fun bin_op_arg1 ((Const (op_,(Type ("fun",
648 [Type (s2,[]),Type ("fun",
649 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
651 fun bin_op_arg2 ((Const (op_,(Type ("fun",
652 [Type (s2,[]),Type ("fun",
653 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
657 exception NO_EQUATION_TERM;
658 fun is_equation ((Const ("op =",(Type ("fun",
659 [Type (_,[]),Type ("fun",
660 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
662 | is_equation _ = false;
663 fun equ_lhs ((Const ("op =",(Type ("fun",
664 [Type (_,[]),Type ("fun",
665 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
667 | equ_lhs _ = raise NO_EQUATION_TERM;
668 fun equ_rhs ((Const ("op =",(Type ("fun",
669 [Type (_,[]),Type ("fun",
670 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
672 | equ_rhs _ = raise NO_EQUATION_TERM;
675 fun atom (Const (_,Type (_,[]))) = true
676 | atom (Free (_,Type (_,[]))) = true
677 | atom (Var (_,Type (_,[]))) = true
678 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
679 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
682 fun varids (Const (s,Type (_,[]))) = [strip_thy s]
683 | varids (Free (s,Type (_,[]))) = if is_no s then []
685 | varids (Var((s,_),Type (_,[]))) = [strip_thy s]
686 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
687 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
688 | varids (Abs(a,T,t)) = union op = [a] (varids t)
689 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
691 (*> val t = term_of (hd (parse Diophant.thy "x"));
692 val t = Free ("x","?DUMMY") : term
694 val it = [] : string list [] !!! *)
697 fun bin_ops_only ((Const op_) $ t1 $ t2) =
698 if(is_bin_op (Const op_))
699 then(bin_ops_only t1)andalso(bin_ops_only t2)
702 if atom t then true else bin_ops_only t;
704 fun polynomial opl t bdVar = (* bdVar TODO *)
705 subset op = (bin_op t, opl) andalso (bin_ops_only t);
707 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
708 andalso polynomial opl (equ_lhs t) bdVar
709 andalso polynomial opl (equ_rhs t) bdVar
710 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
711 subset op = (varids bdVar, varids (equ_lhs t)));
714 let fun max_ m [] = m
715 | max_ m (i::is) = if m<i then max_ i is else max_ m is;
716 in max_ (hd is) is end;
720 fun max (a,b) = if a < b then b else a;
722 fun degree addl mul bdVar t =
724 fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
725 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
726 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
727 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
728 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
729 | deg addl mul v (h $ t1 $ t2) =
730 if subset op = (bin_op h, addl)
731 then max (deg addl mul v t1 ,deg addl mul v t2)
732 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
733 in if polynomial (addl @ [mul]) t bdVar
734 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
736 fun degree_ addl mul bdVar t = (* do not export *)
737 let fun opt (SOME i)= i
739 in opt (degree addl mul bdVar t) end;
742 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
744 fun linear_equ addl mul bdVar t =
746 then let val degl = degree_ addl mul bdVar (equ_lhs t);
747 val degr = degree_ addl mul bdVar (equ_rhs t)
748 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
752 (* strip_thy op_ before *)
753 fun is_div_op (dv,(Const (op_,(Type ("fun",
754 [Type (s2,[]),Type ("fun",
755 [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
756 | is_div_op _ = false;
758 fun is_denom bdVar div_op t =
759 let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
760 | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
761 | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
762 | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
763 | is bool[v]dv (h$n$d) =
765 then (is false[v]dv n)orelse(is true[v]dv d)
766 else (is bool [v]dv n)orelse(is bool[v]dv d)
767 in is false (varids bdVar) (strip_thy div_op) t end;
770 fun rational t div_op bdVar =
771 is_denom bdVar div_op t andalso bin_ops_only t;
776 (** problem types **)
779 (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
780 (["plain_square","univariate","equation","test"],
781 [("#Given" ,["equality e_e","solveFor v_v"]),
782 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
783 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
784 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
785 "(matches ( v_v ^^^2 = 0) e_e)"]),
786 ("#Find" ,["solutions v_v'i'"])
789 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
791 val e_e = (term_of o the o (parse thy)) "e_e::bool";
792 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
795 val pre = (term_of o the o (parse thy))
796 "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
797 "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
798 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
799 "(matches ( v_v ^^^2 = 0, e_e::bool))";
800 val prei = subst_atomic env pre;
801 val cpre = (cterm_of thy) prei;
803 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
804 val ct = "True | False | False | False" : cterm
806 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
807 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
808 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
809 val ct = "True" : cterm
816 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
817 (["polynomial","univariate","equation","test"],
818 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
819 ("#Where" ,["False"]),
820 ("#Find" ,["solutions v_v'i'"])
822 e_rls, SOME "solve (e_e::bool, v_v)", []));
825 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
826 (["degree_two","polynomial","univariate","equation","test"],
827 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
828 ("#Find" ,["solutions v_v'i'"])
830 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
833 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
834 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
835 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
836 ("#Find" ,["solutions v_v'i'"])
838 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
841 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
842 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
843 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
844 ("#Find" ,["solutions v_v'i'"])
846 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
851 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
852 (["squareroot","univariate","equation","test"],
853 [("#Given" ,["equality e_e","solveFor v_v"]),
854 ("#Where" ,["contains_root (e_e::bool)"]),
855 ("#Find" ,["solutions v_v'i'"])
857 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
858 eval_contains_root "#contains_root_")],
859 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]]));
862 (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
863 (["normalize","univariate","equation","test"],
864 [("#Given" ,["equality e_e","solveFor v_v"]),
866 ("#Find" ,["solutions v_v'i'"])
868 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
871 (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
872 (["sqroot-test","univariate","equation","test"],
873 [("#Given" ,["equality e_e","solveFor v_v"]),
874 (*("#Where" ,["contains_root (e_e::bool)"]),*)
875 ("#Find" ,["solutions v_v'i'"])
877 e_rls, SOME "solve (e_e::bool, v_v)", []));
880 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
887 (prep_met thy "met_test_sqrt" [] e_metID
888 (*root-equation, version for tests before 8.01.01*)
889 (["Test","sqrt-equ-test"]:metID,
890 [("#Given" ,["equality e_e","solveFor v_v"]),
891 ("#Where" ,["contains_root (e_e::bool)"]),
892 ("#Find" ,["solutions v_v'i'"])
894 {rew_ord'="e_rew_ord",rls'=tval_rls,
895 srls =append_rls "srls_contains_root" e_rls
896 [Calc ("Test.contains'_root",eval_contains_root "")],
897 prls =append_rls "prls_contains_root" e_rls
898 [Calc ("Test.contains'_root",eval_contains_root "")],
900 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
901 asm_thm=[("square_equation_left",""),
902 ("square_equation_right","")]*)},
903 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
905 " ((While (contains_root e_e) Do" ^
906 " ((Rewrite square_equation_left True) @@" ^
907 " (Try (Rewrite_Set Test_simplify False)) @@" ^
908 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
909 " (Try (Rewrite_Set isolate_root False)) @@" ^
910 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
911 " (Try (Rewrite_Set norm_equation False)) @@" ^
912 " (Try (Rewrite_Set Test_simplify False)) @@" ^
913 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
914 " (Try (Rewrite_Set Test_simplify False)))" ^
922 (prep_met thy "met_test_sqrt2" [] e_metID
923 (*root-equation ... for test-*.sml until 8.01*)
924 (["Test","squ-equ-test2"]:metID,
925 [("#Given" ,["equality e_e","solveFor v_v"]),
926 ("#Find" ,["solutions v_v'i'"])
928 {rew_ord'="e_rew_ord",rls'=tval_rls,
929 srls = append_rls "srls_contains_root" e_rls
930 [Calc ("Test.contains'_root",eval_contains_root"")],
932 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
933 asm_thm=[("square_equation_left",""),
934 ("square_equation_right","")]*)},
935 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
937 " ((While (contains_root e_e) Do" ^
938 " ((Rewrite square_equation_left True) @@" ^
939 " (Try (Rewrite_Set Test_simplify False)) @@" ^
940 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
941 " (Try (Rewrite_Set isolate_root False)) @@" ^
942 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
943 " (Try (Rewrite_Set norm_equation False)) @@" ^
944 " (Try (Rewrite_Set Test_simplify False)) @@" ^
945 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
946 " (Try (Rewrite_Set Test_simplify False)))" ^
948 " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
949 " L_L = Tac solve_equation_dummy " ^
950 " in Check_elementwise L_L {(v_v::real). Assumptions})"
956 (prep_met thy "met_test_squ_sub" [] e_metID
957 (*tests subproblem fixed linear*)
958 (["Test","squ-equ-test-subpbl1"]:metID,
959 [("#Given" ,["equality e_e","solveFor v_v"]),
960 ("#Find" ,["solutions v_v'i'"])
962 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
963 crls=tval_rls, nrls=Test_simplify},
964 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
965 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
966 " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
967 "(L_L::bool list) = (SubProblem (Test', " ^
968 " [linear,univariate,equation,test], " ^
969 " [Test,solve_linear])" ^
970 " [BOOL e_e, REAL v_v])" ^
971 "in Check_elementwise L_L {(v_v::real). Assumptions})"
977 (prep_met thy "met_test_squ_sub2" [] e_metID
978 (*tests subproblem fixed degree 2*)
979 (["Test","squ-equ-test-subpbl2"]:metID,
980 [("#Given" ,["equality e_e","solveFor v_v"]),
981 ("#Find" ,["solutions v_v'i'"])
983 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
984 crls=tval_rls, nrls=e_rls(*,
985 asm_rls=[],asm_thm=[("square_equation_left",""),
986 ("square_equation_right","")]*)},
987 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
988 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
989 "(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
990 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
991 "in Check_elementwise L_L {(v_v::real). Assumptions})"
997 (prep_met thy "met_test_squ_nonterm" [] e_metID
998 (*root-equation: see foils..., but notTerminating*)
999 (["Test","square_equation...notTerminating"]:metID,
1000 [("#Given" ,["equality e_e","solveFor v_v"]),
1001 ("#Find" ,["solutions v_v'i'"])
1003 {rew_ord'="e_rew_ord",rls'=tval_rls,
1004 srls = append_rls "srls_contains_root" e_rls
1005 [Calc ("Test.contains'_root",eval_contains_root"")],
1007 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1008 asm_thm=[("square_equation_left",""),
1009 ("square_equation_right","")]*)},
1010 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1012 " ((While (contains_root e_e) Do" ^
1013 " ((Rewrite square_equation_left True) @@" ^
1014 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1015 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1016 " (Try (Rewrite_Set isolate_root False)) @@" ^
1017 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1018 " (Try (Rewrite_Set norm_equation False)) @@" ^
1019 " (Try (Rewrite_Set Test_simplify False)))" ^
1021 " (L_L::bool list) = " ^
1022 " (SubProblem (Test',[linear,univariate,equation,test]," ^
1023 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1024 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1030 (prep_met thy "met_test_eq1" [] e_metID
1032 (["Test","square_equation1"]:metID,
1033 [("#Given" ,["equality e_e","solveFor v_v"]),
1034 ("#Find" ,["solutions v_v'i'"])
1036 {rew_ord'="e_rew_ord",rls'=tval_rls,
1037 srls = append_rls "srls_contains_root" e_rls
1038 [Calc ("Test.contains'_root",eval_contains_root"")],
1040 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1041 asm_thm=[("square_equation_left",""),
1042 ("square_equation_right","")]*)},
1043 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1045 " ((While (contains_root e_e) Do" ^
1046 " ((Rewrite square_equation_left True) @@" ^
1047 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1048 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1049 " (Try (Rewrite_Set isolate_root False)) @@" ^
1050 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1051 " (Try (Rewrite_Set norm_equation False)) @@" ^
1052 " (Try (Rewrite_Set Test_simplify False)))" ^
1054 " (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
1055 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1056 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1062 (prep_met thy "met_test_squ2" [] e_metID
1064 (["Test","square_equation2"]:metID,
1065 [("#Given" ,["equality e_e","solveFor v_v"]),
1066 ("#Find" ,["solutions v_v'i'"])
1068 {rew_ord'="e_rew_ord",rls'=tval_rls,
1069 srls = append_rls "srls_contains_root" e_rls
1070 [Calc ("Test.contains'_root",eval_contains_root"")],
1072 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1073 asm_thm=[("square_equation_left",""),
1074 ("square_equation_right","")]*)},
1075 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1077 " ((While (contains_root e_e) Do" ^
1078 " (((Rewrite square_equation_left True) Or " ^
1079 " (Rewrite square_equation_right True)) @@" ^
1080 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1081 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1082 " (Try (Rewrite_Set isolate_root False)) @@" ^
1083 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1084 " (Try (Rewrite_Set norm_equation False)) @@" ^
1085 " (Try (Rewrite_Set Test_simplify False)))" ^
1087 " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
1088 " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
1089 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1095 (prep_met thy "met_test_squeq" [] e_metID
1097 (["Test","square_equation"]:metID,
1098 [("#Given" ,["equality e_e","solveFor v_v"]),
1099 ("#Find" ,["solutions v_v'i'"])
1101 {rew_ord'="e_rew_ord",rls'=tval_rls,
1102 srls = append_rls "srls_contains_root" e_rls
1103 [Calc ("Test.contains'_root",eval_contains_root"")],
1105 crls=tval_rls, nrls=e_rls(*,asm_rls=[],
1106 asm_thm=[("square_equation_left",""),
1107 ("square_equation_right","")]*)},
1108 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1110 " ((While (contains_root e_e) Do" ^
1111 " (((Rewrite square_equation_left True) Or" ^
1112 " (Rewrite square_equation_right True)) @@" ^
1113 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1114 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1115 " (Try (Rewrite_Set isolate_root False)) @@" ^
1116 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1117 " (Try (Rewrite_Set norm_equation False)) @@" ^
1118 " (Try (Rewrite_Set Test_simplify False)))" ^
1120 " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
1121 " [no_met]) [BOOL e_e, REAL v_v])" ^
1122 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1128 (prep_met thy "met_test_eq_plain" [] e_metID
1129 (*solve_plain_square*)
1130 (["Test","solve_plain_square"]:metID,
1131 [("#Given",["equality e_e","solveFor v_v"]),
1132 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1133 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1134 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1135 "(matches ( v_v ^^^2 = 0) e_e)"]),
1136 ("#Find" ,["solutions v_v'i'"])
1138 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
1139 prls = assoc_rls "matches",
1140 crls=tval_rls, nrls=e_rls(*,
1141 asm_rls=[],asm_thm=[]*)},
1142 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
1143 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
1144 " (Try (Rewrite_Set Test_simplify False)) @@ " ^
1145 " ((Rewrite square_equality_0 False) Or " ^
1146 " (Rewrite square_equality True)) @@ " ^
1147 " (Try (Rewrite_Set tval_rls False))) e_e " ^
1148 " in ((Or_to_List e_e)::bool list))"
1154 (prep_met thy "met_test_norm_univ" [] e_metID
1155 (["Test","norm_univar_equation"]:metID,
1156 [("#Given",["equality e_e","solveFor v_v"]),
1158 ("#Find" ,["solutions v_v'i'"])
1160 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
1162 crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
1163 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1164 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1165 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1166 " in (SubProblem (Test',[univariate,equation,test], " ^
1167 " [no_met]) [BOOL e_e, REAL v_v]))"
1172 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1176 (*8.4.03 aus Poly.ML--------------------------------vvv---
1177 make_polynomial ---> make_poly
1178 ^-- for user ^-- for systest _ONLY_*)
1180 local (*. for make_polytest .*)
1182 open Term; (* for type order = EQUAL | LESS | GREATER *)
1184 fun pr_ord EQUAL = "EQUAL"
1185 | pr_ord LESS = "LESS"
1186 | pr_ord GREATER = "GREATER";
1188 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1190 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1191 | _ => (((a, 0), T), 0))
1192 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1193 | dest_hd' (Var v) = (v, 2)
1194 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1195 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1197 fun get_order_pow (t $ (Free(order,_))) =
1198 (case int_of_str (order) of
1201 | get_order_pow _ = 0;
1203 fun size_of_term' (Const(str,_) $ t) =
1204 if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
1205 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1206 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1207 | size_of_term' _ = 1;
1209 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1210 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1211 | term_ord' pr thy (t, u) =
1214 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1215 val _=tracing("t= f@ts= " ^ "" ^
1216 ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^
1217 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\"");
1218 val _=tracing("u= g@us= " ^ "" ^
1219 ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^
1220 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
1221 val _=tracing("size_of_term(t,u)= ("^
1222 (string_of_int(size_of_term' t)) ^ ", " ^
1223 (string_of_int(size_of_term' u)) ^ ")");
1224 val _=tracing("hd_ord(f,g) = " ^ ((pr_ord o hd_ord)(f,g)));
1225 val _=tracing("terms_ord(ts,us) = " ^
1226 ((pr_ord o terms_ord str false)(ts,us)));
1227 val _=tracing("-------");
1230 case int_ord (size_of_term' t, size_of_term' u) of
1232 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1233 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1237 and hd_ord (f, g) = (* ~ term.ML *)
1238 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1239 and terms_ord str pr (ts, us) =
1240 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
1243 fun ord_make_polytest (pr:bool) thy (_:subst) tu =
1244 (term_ord' pr thy(***) tu = LESS );
1250 rew_ord' := overwritel (!rew_ord',
1251 [("termlessI", termlessI),
1252 ("ord_make_polytest", ord_make_polytest false thy)
1255 (*WN060510 this was a preparation for prep_rls ...
1256 val scr_make_polytest =
1257 "Script Expand_binomtest t_t =" ^
1259 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1261 " (Try (Repeat (Rewrite left_distrib False))) @@ " ^
1262 " (Try (Repeat (Rewrite right_distrib False))) @@ " ^
1263 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
1264 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
1266 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1267 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1268 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1270 " (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
1271 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
1272 " (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
1273 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
1274 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
1275 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
1277 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1278 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1279 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1280 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1282 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1283 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1285 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1286 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1288 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1289 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1290 " (Try (Repeat (Calculate POWER)))) " ^
1292 -----------------------------------------------------*)
1295 Rls{id = "make_polytest", preconds = []:term list,
1296 rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
1297 erls = testerls, srls = Erls,
1298 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1299 ("TIMES" , ("op *", eval_binop "#mult_")),
1300 ("POWER", ("Atools.pow", eval_binop "#power_"))
1303 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
1304 (*"a - b = a + (-1) * b"*)
1305 Thm ("left_distrib" ,num_str @{thm left_distrib}),
1306 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1307 Thm ("right_distrib",num_str @{thm right_distrib}),
1308 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1309 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1310 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1311 Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1312 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1313 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1315 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1317 Thm ("add_0_left",num_str @{thm add_0_left}),
1321 Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
1323 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1324 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1325 Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
1326 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1327 Thm ("add_commute",num_str @{thm add_commute}),
1329 Thm ("add_left_commute",num_str @{thm add_left_commute}),
1330 (*x + (y + z) = y + (x + z)*)
1331 Thm ("add_assoc",num_str @{thm add_assoc}),
1332 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1334 Thm ("sym_realpow_twoI",
1335 num_str (@{thm realpow_twoI} RS @{thm sym})),
1336 (*"r1 * r1 = r1 ^^^ 2"*)
1337 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1338 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1339 Thm ("sym_real_mult_2",
1340 num_str (@{thm real_mult_2} RS @{thm sym})),
1341 (*"z1 + z1 = 2 * z1"*)
1342 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1343 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1345 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1346 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1347 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1348 (*"[| l is_const; m is_const |] ==>
1349 l * n + (m * n + k) = (l + m) * n + k"*)
1350 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1351 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1352 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1353 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1355 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1356 Calc ("op *", eval_binop "#mult_"),
1357 Calc ("Atools.pow", eval_binop "#power_")
1359 scr = EmptyScr(*Script ((term_of o the o (parse thy))
1360 scr_make_polytest)*)
1364 (*WN060510 this was done before 'fun prep_rls' ...------------------------
1365 val scr_expand_binomtest =
1366 "Script Expand_binomtest t_t =" ^
1368 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
1369 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
1370 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
1371 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
1372 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
1373 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
1375 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1376 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1377 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1379 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1380 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1381 " (Try (Repeat (Calculate POWER))) @@ " ^
1383 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1384 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1385 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1386 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1388 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1389 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1391 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1392 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1394 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1395 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1396 " (Try (Repeat (Calculate POWER)))) " ^
1398 --------------------------------------------------------------------------*)
1400 val expand_binomtest =
1401 Rls{id = "expand_binomtest", preconds = [],
1402 rew_ord = ("termlessI",termlessI),
1403 erls = testerls, srls = Erls,
1404 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1405 ("TIMES" , ("op *", eval_binop "#mult_")),
1406 ("POWER", ("Atools.pow", eval_binop "#power_"))
1409 [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
1410 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1411 Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1412 (*"(a + b)*(a + b) = ...*)
1413 Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
1414 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1415 Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
1416 (*"(a - b)*(a - b) = ...*)
1417 Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
1418 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1419 Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
1420 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1422 Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1423 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1424 Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1425 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1426 Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1427 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1428 Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1429 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1430 Thm ("realpow_multI",num_str @{thm realpow_multI}),
1431 (*(a*b)^^^n = a^^^n * b^^^n*)
1432 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1433 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1434 Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
1435 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1438 (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
1439 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1440 Thm ("right_distrib",num_str @{thm right_distrib}),
1441 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1442 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1443 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1444 Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1445 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1448 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1450 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1452 Thm ("add_0_left",num_str @{thm add_0_left}),
1455 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1456 Calc ("op *", eval_binop "#mult_"),
1457 Calc ("Atools.pow", eval_binop "#power_"),
1459 Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
1461 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1462 Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
1463 Thm ("add_commute",num_str @{thm add_commute}),
1464 Thm ("add_left_commute",num_str @{thm add_left_commute}),
1465 Thm ("add_assoc",num_str @{thm add_assoc}),
1468 Thm ("sym_realpow_twoI",
1469 num_str (@{thm realpow_twoI} RS @{thm sym})),
1470 (*"r1 * r1 = r1 ^^^ 2"*)
1471 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1472 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1473 (*Thm ("sym_real_mult_2",
1474 num_str (@{thm real_mult_2} RS @{thm sym})),
1475 (*"z1 + z1 = 2 * z1"*)*)
1476 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1477 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1479 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1480 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1481 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1482 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1483 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1484 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1485 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1486 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1488 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1489 Calc ("op *", eval_binop "#mult_"),
1490 Calc ("Atools.pow", eval_binop "#power_")
1493 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
1497 ruleset' := overwritelthy @{theory} (!ruleset',
1498 [("make_polytest", prep_rls make_polytest),
1499 ("expand_binomtest", prep_rls expand_binomtest)