cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
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)
35 "precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
36 "precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
37 "precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
38 "precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
42 bool list] => bool list"
43 ("((Script Solve'_root'_equation (_ _ =))//
48 bool list] => bool list"
49 ("((Script Solve'_plain'_square (_ _ =))//
52 Norm'_univar'_equation
55 ("((Script Norm'_univar'_equation (_ _ =))//
61 ("((Script STest'_simplify (_ =))//
64 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
66 axiomatization where (*TODO: prove as theorems*)
68 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
69 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
70 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
71 rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
73 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
75 "m is_const ==> (n::real) + m * n = (1 + m) * n" and
76 rcollect_one_left_assoc:
77 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
78 rcollect_one_left_assoc_p:
79 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
81 rtwo_of_the_same: "a + a = 2 * a" and
82 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
83 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
85 rcancel_den: "not(a=0) ==> a * (b / a) = b" and
86 rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
87 rshift_nominator: "(a::real) * b / c = a / c * b" and
89 exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
90 rsqare: "(a::real) * a = a ^^^ 2" and
91 power_1: "(a::real) ^^^ 1 = a" and
92 rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and
94 rmult_1: "1 * k = (k::real)" and
95 rmult_1_right: "k * 1 = (k::real)" and
96 rmult_0: "0 * k = (0::real)" and
97 rmult_0_right: "k * 0 = (0::real)" and
98 radd_0: "0 + k = (k::real)" and
99 radd_0_right: "k + 0 = (k::real)" and
102 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
104 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
107 radd_commute: "(m::real) + (n::real) = n + m" and
108 radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
109 radd_assoc: "(m::real) + n + k = m + (n + k)" and
110 rmult_commute: "(m::real) * n = n * m" and
111 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
112 rmult_assoc: "(m::real) * n * k = m * (n * k)" and
114 (*for equations: 'bdv' is a meta-constant*)
115 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
116 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
117 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
120 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
122 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
123 root_ge0: "0 <= a ==> 0 <= sqrt a" and
124 (*should be dropped with better simplification in eval_rls ...*)
126 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
128 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
130 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
133 rroot_square_inv: "(sqrt a)^^^ 2 = a" and
134 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
135 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
136 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
139 (*for root-equations*)
140 square_equation_left:
141 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and
142 square_equation_right:
143 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and
144 (*causes frequently non-termination:*)
146 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and
148 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
149 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
150 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
152 (*for polynomial equations of degree 2; linear case in RatArith*)
153 mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and
154 constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and
155 constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and
158 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
160 "(x^^^2 = 0) = (x = 0)" and
162 (*isolate root on the LEFT hand side of the equation
163 otherwise shuffling from left to right would not terminate*)
166 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
168 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
169 rroot_to_lhs_add_mult:
170 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
171 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
176 (** evaluation of numerals and predicates **)
178 (*does a term contain a root ? WN110518 seems incorrect, compare contains_root*)
179 fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy =
180 if strip_thy op0 <> "is'_root'_free"
181 then error ("eval_root_free: wrong " ^ op0)
182 else if const_in (strip_thy op0) arg
183 then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
184 Trueprop $ (mk_equality (t, @{term False})))
185 else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
186 Trueprop $ (mk_equality (t, @{term True})))
187 | eval_root_free _ _ _ _ = NONE;
189 (*does a term contain a root ?*)
190 fun eval_contains_root (thmid:string) _
191 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
192 if member op = (ids_of arg) "sqrt"
193 then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
194 Trueprop $ (mk_equality (t, @{term True})))
195 else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
196 Trueprop $ (mk_equality (t, @{term False})))
197 | eval_contains_root _ _ _ _ = NONE;
199 (*dummy precondition for root-met of x+1=2*)
200 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
201 SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
202 Trueprop $ (mk_equality (t, @{term True})))
203 | eval_precond_rootmet _ _ _ _ = NONE;
205 (*dummy precondition for root-pbl of x+1=2*)
206 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
207 SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
208 Trueprop $ (mk_equality (t, @{term True})))
209 | eval_precond_rootpbl _ _ _ _ = NONE;
211 setup {* KEStore_Elems.add_calcs
212 [("is_root_free", ("Test.is'_root'_free", eval_root_free"#is_root_free_e")),
213 ("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
214 ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
215 ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
216 eval_precond_rootpbl"#Test.precond_rootpbl_"))] *}
219 fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
224 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
225 erls = e_rls, srls = Erls,
226 calc = [], errpatts = [],
227 rules = [Thm ("refl",num_str @{thm refl}),
228 Thm ("order_refl",num_str @{thm order_refl}),
229 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
230 Thm ("not_true",num_str @{thm not_true}),
231 Thm ("not_false",num_str @{thm not_false}),
232 Thm ("and_true",num_str @{thm and_true}),
233 Thm ("and_false",num_str @{thm and_false}),
234 Thm ("or_true",num_str @{thm or_true}),
235 Thm ("or_false",num_str @{thm or_false}),
236 Thm ("and_commute",num_str @{thm and_commute}),
237 Thm ("or_commute",num_str @{thm or_commute}),
239 Calc ("Atools.is'_const",eval_const "#is_const_"),
240 Calc ("Tools.matches",eval_matches ""),
242 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
243 Calc ("Groups.times_class.times",eval_binop "#mult_"),
244 Calc ("Atools.pow" ,eval_binop "#power_"),
246 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
247 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
249 Calc ("Atools.ident",eval_ident "#ident_")],
250 scr = Prog ((term_of o the o (parse thy)) "empty_script")
254 (*.for evaluation of conditions in rewrite rules.*)
255 (*FIXXXXXXME 10.8.02: handle like _simplify*)
257 Rls{id = "tval_rls", preconds = [],
258 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
259 erls=testerls,srls = e_rls,
260 calc=[], errpatts = [],
261 rules = [Thm ("refl",num_str @{thm refl}),
262 Thm ("order_refl",num_str @{thm order_refl}),
263 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
264 Thm ("not_true",num_str @{thm not_true}),
265 Thm ("not_false",num_str @{thm not_false}),
266 Thm ("and_true",num_str @{thm and_true}),
267 Thm ("and_false",num_str @{thm and_false}),
268 Thm ("or_true",num_str @{thm or_true}),
269 Thm ("or_false",num_str @{thm or_false}),
270 Thm ("and_commute",num_str @{thm and_commute}),
271 Thm ("or_commute",num_str @{thm or_commute}),
273 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
275 Thm ("root_ge0",num_str @{thm root_ge0}),
276 Thm ("root_add_ge0",num_str @{thm root_add_ge0}),
277 Thm ("root_ge0_1",num_str @{thm root_ge0_1}),
278 Thm ("root_ge0_2",num_str @{thm root_ge0_2}),
280 Calc ("Atools.is'_const",eval_const "#is_const_"),
281 Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_e"),
282 Calc ("Tools.matches",eval_matches ""),
283 Calc ("Test.contains'_root",
284 eval_contains_root"#contains_root_"),
286 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
287 Calc ("Groups.times_class.times",eval_binop "#mult_"),
288 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
289 Calc ("Atools.pow" ,eval_binop "#power_"),
291 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
292 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
294 Calc ("Atools.ident",eval_ident "#ident_")],
295 scr = Prog ((term_of o the o (parse thy)) "empty_script")
298 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *}
301 (*make () dissappear*)
302 val rearrange_assoc =
303 Rls{id = "rearrange_assoc", preconds = [],
304 rew_ord = ("e_rew_ord",e_rew_ord),
305 erls = e_rls, srls = e_rls, calc = [], errpatts = [],
307 [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
308 Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
309 scr = Prog ((term_of o the o (parse thy)) "empty_script")
313 Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
314 erls = e_rls, srls = e_rls, calc = [], errpatts = [],
316 [Thm ("radd_commute",num_str @{thm radd_commute}),
317 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
318 Thm ("add_assoc",num_str @{thm add_assoc}),
319 Thm ("rmult_commute",num_str @{thm rmult_commute}),
320 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
321 Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
322 scr = Prog ((term_of o the o (parse thy)) "empty_script")
325 (*todo: replace by Rewrite("rnorm_equation_add",num_str @{thm rnorm_equation_add)*)
327 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
328 erls = tval_rls, srls = e_rls, calc = [], errpatts = [],
329 rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
331 scr = Prog ((term_of o the o (parse thy)) "empty_script")
337 val STest_simplify = (* vv--- not changed to real by parse*)
338 "Script STest_simplify (t_t::'z) = " ^
340 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
341 " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
342 " (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ " ^
343 " (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^
344 " (Try (Repeat (Rewrite rdistr_div_right False))) @@ " ^
345 " (Try (Repeat (Rewrite rbinom_power_2 False))) @@ " ^
347 " (Try (Repeat (Rewrite radd_commute False))) @@ " ^
348 " (Try (Repeat (Rewrite radd_left_commute False))) @@ " ^
349 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
350 " (Try (Repeat (Rewrite rmult_commute False))) @@ " ^
351 " (Try (Repeat (Rewrite rmult_left_commute False))) @@ " ^
352 " (Try (Repeat (Rewrite rmult_assoc False))) @@ " ^
354 " (Try (Repeat (Rewrite radd_real_const_eq False))) @@ " ^
355 " (Try (Repeat (Rewrite radd_real_const False))) @@ " ^
356 " (Try (Repeat (Calculate PLUS))) @@ " ^
357 " (Try (Repeat (Calculate TIMES))) @@ " ^
358 " (Try (Repeat (Calculate divide_))) @@" ^
359 " (Try (Repeat (Calculate POWER))) @@ " ^
361 " (Try (Repeat (Rewrite rcollect_right False))) @@ " ^
362 " (Try (Repeat (Rewrite rcollect_one_left False))) @@ " ^
363 " (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ " ^
364 " (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ " ^
366 " (Try (Repeat (Rewrite rshift_nominator False))) @@ " ^
367 " (Try (Repeat (Rewrite rcancel_den False))) @@ " ^
368 " (Try (Repeat (Rewrite rroot_square_inv False))) @@ " ^
369 " (Try (Repeat (Rewrite rroot_times_root False))) @@ " ^
370 " (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ " ^
371 " (Try (Repeat (Rewrite rsqare False))) @@ " ^
372 " (Try (Repeat (Rewrite power_1 False))) @@ " ^
373 " (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ " ^
374 " (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ " ^
376 " (Try (Repeat (Rewrite rmult_1 False))) @@ " ^
377 " (Try (Repeat (Rewrite rmult_1_right False))) @@ " ^
378 " (Try (Repeat (Rewrite rmult_0 False))) @@ " ^
379 " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
380 " (Try (Repeat (Rewrite radd_0 False))) @@ " ^
381 " (Try (Repeat (Rewrite radd_0_right False)))) " ^
386 (* expects * distributed over + *)
388 Rls{id = "Test_simplify", preconds = [],
389 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
390 erls = tval_rls, srls = e_rls,
391 calc=[(*since 040209 filled by prep_rls*)], errpatts = [],
393 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
394 Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}),
395 Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}),
396 Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}),
397 Thm ("rdistr_div_right",num_str @{thm rdistr_div_right}),
398 Thm ("rbinom_power_2",num_str @{thm rbinom_power_2}),
400 Thm ("radd_commute",num_str @{thm radd_commute}),
401 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
402 Thm ("add_assoc",num_str @{thm add_assoc}),
403 Thm ("rmult_commute",num_str @{thm rmult_commute}),
404 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
405 Thm ("rmult_assoc",num_str @{thm rmult_assoc}),
407 Thm ("radd_real_const_eq",num_str @{thm radd_real_const_eq}),
408 Thm ("radd_real_const",num_str @{thm radd_real_const}),
409 (* these 2 rules are invers to distr_div_right wrt. termination.
410 thus they MUST be done IMMEDIATELY before calc *)
411 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
412 Calc ("Groups.times_class.times", eval_binop "#mult_"),
413 Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
414 Calc ("Atools.pow", eval_binop "#power_"),
416 Thm ("rcollect_right",num_str @{thm rcollect_right}),
417 Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}),
418 Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}),
419 Thm ("rcollect_one_left_assoc_p",num_str @{thm rcollect_one_left_assoc_p}),
421 Thm ("rshift_nominator",num_str @{thm rshift_nominator}),
422 Thm ("rcancel_den",num_str @{thm rcancel_den}),
423 Thm ("rroot_square_inv",num_str @{thm rroot_square_inv}),
424 Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
425 Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
426 Thm ("rsqare",num_str @{thm rsqare}),
427 Thm ("power_1",num_str @{thm power_1}),
428 Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
429 Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
431 Thm ("rmult_1",num_str @{thm rmult_1}),
432 Thm ("rmult_1_right",num_str @{thm rmult_1_right}),
433 Thm ("rmult_0",num_str @{thm rmult_0}),
434 Thm ("rmult_0_right",num_str @{thm rmult_0_right}),
435 Thm ("radd_0",num_str @{thm radd_0}),
436 Thm ("radd_0_right",num_str @{thm radd_0_right})
438 scr = Prog ((term_of o the o (parse thy)) "empty_script")
439 (*since 040209 filled by prep_rls: STest_simplify*)
448 (*isolate the root in a root-equation*)
450 Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
451 erls=tval_rls,srls = e_rls, calc=[], errpatts = [],
452 rules = [Thm ("rroot_to_lhs",num_str @{thm rroot_to_lhs}),
453 Thm ("rroot_to_lhs_mult",num_str @{thm rroot_to_lhs_mult}),
454 Thm ("rroot_to_lhs_add_mult",num_str @{thm rroot_to_lhs_add_mult}),
455 Thm ("risolate_root_add",num_str @{thm risolate_root_add}),
456 Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),
457 Thm ("risolate_root_div",num_str @{thm risolate_root_div}) ],
458 scr = Prog ((term_of o the o (parse thy))
462 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
464 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
465 erls=tval_rls,srls = e_rls, calc= [], errpatts = [],
467 [Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
468 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
469 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
470 Thm ("mult_square",num_str @{thm mult_square}),
471 Thm ("constant_square",num_str @{thm constant_square}),
472 Thm ("constant_mult_square",num_str @{thm constant_mult_square})
474 scr = Prog ((term_of o the o (parse thy))
480 (* association list for calculate_, calculate
481 "Groups.plus_class.plus" etc. not usable in scripts *)
485 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
486 ("matches",("Tools.matches",eval_matches "#matches_")),
487 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
489 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
490 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
491 ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
492 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
493 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
494 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
495 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
496 ("ident" ,("Atools.ident",eval_ident "#ident_")),
497 (*von hier (ehem.SqRoot*)
498 ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
499 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),
500 ("Test.contains_root",("contains'_root",
501 eval_contains_root"#contains_root_"))
504 setup {* KEStore_Elems.add_rlss
505 [("Test_simplify", (Context.theory_name @{theory}, prep_rls Test_simplify)),
506 ("tval_rls", (Context.theory_name @{theory}, prep_rls tval_rls)),
507 ("isolate_root", (Context.theory_name @{theory}, prep_rls isolate_root)),
508 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls isolate_bdv)),
509 ("matches", (Context.theory_name @{theory}, prep_rls
510 (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *}
513 (** problem types **)
515 (prep_pbt thy "pbl_test" [] e_pblID
520 (prep_pbt thy "pbl_test_equ" [] e_pblID
521 (["equation","test"],
522 [("#Given" ,["equality e_e","solveFor v_v"]),
523 ("#Where" ,["matches (?a = ?b) e_e"]),
524 ("#Find" ,["solutions v_v'i'"])
526 assoc_rls' @{theory} "matches",
527 SOME "solve (e_e::bool, v_v)", []));
530 (prep_pbt thy "pbl_test_uni" [] e_pblID
531 (["univariate","equation","test"],
532 [("#Given" ,["equality e_e","solveFor v_v"]),
533 ("#Where" ,["matches (?a = ?b) e_e"]),
534 ("#Find" ,["solutions v_v'i'"])
536 assoc_rls' @{theory} "matches",
537 SOME "solve (e_e::bool, v_v)", []));
540 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
541 (["LINEAR","univariate","equation","test"],
542 [("#Given" ,["equality e_e","solveFor v_v"]),
543 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
544 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
545 ("#Find" ,["solutions v_v'i'"])
547 assoc_rls' @{theory} "matches",
548 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
554 [("#Given" ,"boolTestGiven g_g"),
555 ("#Find" ,"boolTestFind f_f")
562 [("#Given" ,"boolTestGiven g_g"),
563 ("#Find" ,"boolTestFind f_f")
568 val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
573 setup {* KEStore_Elems.add_pbts
574 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
575 (prep_pbt thy "pbl_test_equ" [] e_pblID
576 (["equation","test"],
577 [("#Given" ,["equality e_e","solveFor v_v"]),
578 ("#Where" ,["matches (?a = ?b) e_e"]),
579 ("#Find" ,["solutions v_v'i'"])],
580 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
581 (prep_pbt thy "pbl_test_uni" [] e_pblID
582 (["univariate","equation","test"],
583 [("#Given" ,["equality e_e","solveFor v_v"]),
584 ("#Where" ,["matches (?a = ?b) e_e"]),
585 ("#Find" ,["solutions v_v'i'"])],
586 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
587 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
588 (["LINEAR","univariate","equation","test"],
589 [("#Given" ,["equality e_e","solveFor v_v"]),
590 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
591 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
592 ("#Find" ,["solutions v_v'i'"])],
593 assoc_rls' @{theory} "matches",
594 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))(*,
597 [("#Given" ,"boolTestGiven g_g"),
598 ("#Find" ,"boolTestFind f_f")],
602 [("#Given" ,"boolTestGiven g_g"),
603 ("#Find" ,"boolTestFind f_f")],
608 (prep_met @{theory "Diff"} "met_test" [] e_metID
611 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
612 crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"));
616 (prep_met thy "met_test_solvelin" [] e_metID
617 (["Test","solve_linear"]:metID,
618 [("#Given" ,["equality e_e","solveFor v_v"]),
619 ("#Where" ,["matches (?a = ?b) e_e"]),
620 ("#Find" ,["solutions v_v'i'"])
622 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
623 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls,
624 errpats = [], nrls = Test_simplify},
625 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
628 " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
629 " (Rewrite_Set Test_simplify False))) e_e" ^
632 (*, prep_met thy (*test for equations*)
633 (["Test","testeq"]:metID,
634 [("#Given" ,["boolTestGiven g_g"]),
635 ("#Find" ,["boolTestFind f_f"])
637 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
638 asm_thm=[("square_equation_left","")]},
639 "Script Testeq (e_q::bool) = " ^
641 " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
642 " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
643 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
644 " in e_e) Until (is_root_free e_e)" (*deleted*)
650 setup {* KEStore_Elems.add_rlss
651 [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)),
652 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls ac_plus_times)),
653 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls rearrange_assoc))] *}
657 fun bin_o (Const (op_,(Type ("fun",
658 [Type (s2,[]),Type ("fun",
659 [Type (s4,tl4),Type (s5,tl5)])])))) =
660 if (s2=s4)andalso(s4=s5)then[op_]else[]
663 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
664 | bin_op t = bin_o t;
665 fun is_bin_op t = ((bin_op t)<>[]);
667 fun bin_op_arg1 ((Const (op_,(Type ("fun",
668 [Type (s2,[]),Type ("fun",
669 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
671 fun bin_op_arg2 ((Const (op_,(Type ("fun",
672 [Type (s2,[]),Type ("fun",
673 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
677 exception NO_EQUATION_TERM;
678 fun is_equation ((Const ("HOL.eq",(Type ("fun",
679 [Type (_,[]),Type ("fun",
680 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
682 | is_equation _ = false;
683 fun equ_lhs ((Const ("HOL.eq",(Type ("fun",
684 [Type (_,[]),Type ("fun",
685 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
687 | equ_lhs _ = raise NO_EQUATION_TERM;
688 fun equ_rhs ((Const ("HOL.eq",(Type ("fun",
689 [Type (_,[]),Type ("fun",
690 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
692 | equ_rhs _ = raise NO_EQUATION_TERM;
695 fun atom (Const (_,Type (_,[]))) = true
696 | atom (Free (_,Type (_,[]))) = true
697 | atom (Var (_,Type (_,[]))) = true
698 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
699 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
702 fun varids (Const (s,Type (_,[]))) = [strip_thy s]
703 | varids (Free (s,Type (_,[]))) = if is_no s then []
705 | varids (Var((s,_),Type (_,[]))) = [strip_thy s]
706 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
707 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
708 | varids (Abs(a,T,t)) = union op = [a] (varids t)
709 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
711 (*> val t = term_of (hd (parse Diophant.thy "x"));
712 val t = Free ("x","?DUMMY") : term
714 val it = [] : string list [] !!! *)
717 fun bin_ops_only ((Const op_) $ t1 $ t2) =
718 if(is_bin_op (Const op_))
719 then(bin_ops_only t1)andalso(bin_ops_only t2)
722 if atom t then true else bin_ops_only t;
724 fun polynomial opl t bdVar = (* bdVar TODO *)
725 subset op = (bin_op t, opl) andalso (bin_ops_only t);
727 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
728 andalso polynomial opl (equ_lhs t) bdVar
729 andalso polynomial opl (equ_rhs t) bdVar
730 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
731 subset op = (varids bdVar, varids (equ_lhs t)));
734 let fun max_ m [] = m
735 | max_ m (i::is) = if m<i then max_ i is else max_ m is;
736 in max_ (hd is) is end;
740 fun max (a,b) = if a < b then b else a;
742 fun degree addl mul bdVar t =
744 fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
745 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
746 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
747 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
748 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
749 | deg addl mul v (h $ t1 $ t2) =
750 if subset op = (bin_op h, addl)
751 then max (deg addl mul v t1 ,deg addl mul v t2)
752 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
753 in if polynomial (addl @ [mul]) t bdVar
754 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
756 fun degree_ addl mul bdVar t = (* do not export *)
757 let fun opt (SOME i)= i
759 in opt (degree addl mul bdVar t) end;
762 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
764 fun linear_equ addl mul bdVar t =
766 then let val degl = degree_ addl mul bdVar (equ_lhs t);
767 val degr = degree_ addl mul bdVar (equ_rhs t)
768 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
772 (* strip_thy op_ before *)
773 fun is_div_op (dv,(Const (op_,(Type ("fun",
774 [Type (s2,[]),Type ("fun",
775 [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
776 | is_div_op _ = false;
778 fun is_denom bdVar div_op t =
779 let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
780 | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
781 | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
782 | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
783 | is bool[v]dv (h$n$d) =
785 then (is false[v]dv n)orelse(is true[v]dv d)
786 else (is bool [v]dv n)orelse(is bool[v]dv d)
787 in is false (varids bdVar) (strip_thy div_op) t end;
790 fun rational t div_op bdVar =
791 is_denom bdVar div_op t andalso bin_ops_only t;
796 (** problem types **)
799 (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
800 (["plain_square","univariate","equation","test"],
801 [("#Given" ,["equality e_e","solveFor v_v"]),
802 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
803 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
804 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
805 "(matches ( v_v ^^^2 = 0) e_e)"]),
806 ("#Find" ,["solutions v_v'i'"])
808 assoc_rls' @{theory} "matches",
809 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
811 val e_e = (term_of o the o (parse thy)) "e_e::bool";
812 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
815 val pre = (term_of o the o (parse thy))
816 "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
817 "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
818 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
819 "(matches ( v_v ^^^2 = 0, e_e::bool))";
820 val prei = subst_atomic env pre;
821 val cpre = (cterm_of thy) prei;
823 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
824 val ct = "True | False | False | False" : cterm
826 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
827 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
828 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
829 val ct = "HOL.True" : cterm
834 setup {* KEStore_Elems.add_pbts
835 [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
836 (["plain_square","univariate","equation","test"],
837 [("#Given" ,["equality e_e","solveFor v_v"]),
838 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
839 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
840 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
841 "(matches ( v_v ^^^2 = 0) e_e)"]),
842 ("#Find" ,["solutions v_v'i'"])],
843 assoc_rls' @{theory} "matches",
844 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
847 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
848 (["polynomial","univariate","equation","test"],
849 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
850 ("#Where" ,["HOL.False"]),
851 ("#Find" ,["solutions v_v'i'"])
853 e_rls, SOME "solve (e_e::bool, v_v)", []));
856 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
857 (["degree_two","polynomial","univariate","equation","test"],
858 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
859 ("#Find" ,["solutions v_v'i'"])
861 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
864 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
865 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
866 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
867 ("#Find" ,["solutions v_v'i'"])
869 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
872 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
873 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
874 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
875 ("#Find" ,["solutions v_v'i'"])
877 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
882 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
883 (["squareroot","univariate","equation","test"],
884 [("#Given" ,["equality e_e","solveFor v_v"]),
885 ("#Where" ,["precond_rootpbl v_v"]),
886 ("#Find" ,["solutions v_v'i'"])
888 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
889 eval_contains_root "#contains_root_")],
890 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]]));
893 (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
894 (["normalize","univariate","equation","test"],
895 [("#Given" ,["equality e_e","solveFor v_v"]),
897 ("#Find" ,["solutions v_v'i'"])
899 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
902 (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
903 (["sqroot-test","univariate","equation","test"],
904 [("#Given" ,["equality e_e","solveFor v_v"]),
905 ("#Where" ,["precond_rootpbl v_v"]),
906 ("#Find" ,["solutions v_v'i'"])
908 e_rls, SOME "solve (e_e::bool, v_v)", []));
911 (prep_pbt thy "pbl_test_intsimp" [] e_pblID
913 [("#Given" ,["intTestGiven t_t"]),
915 ("#Find" ,["intTestFind s_s"])
917 e_rls, NONE, [["Test","intsimp"]]));
920 get_pbt ["inttype","test"];
924 setup {* KEStore_Elems.add_pbts
925 [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
926 (["polynomial","univariate","equation","test"],
927 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
928 ("#Where" ,["HOL.False"]),
929 ("#Find" ,["solutions v_v'i'"])],
930 e_rls, SOME "solve (e_e::bool, v_v)", [])),
931 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
932 (["degree_two","polynomial","univariate","equation","test"],
933 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
934 ("#Find" ,["solutions v_v'i'"])],
935 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
936 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
937 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
938 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
939 ("#Find" ,["solutions v_v'i'"])],
940 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
941 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
942 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
943 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
944 ("#Find" ,["solutions v_v'i'"])],
945 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
946 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
947 (["squareroot","univariate","equation","test"],
948 [("#Given" ,["equality e_e","solveFor v_v"]),
949 ("#Where" ,["precond_rootpbl v_v"]),
950 ("#Find" ,["solutions v_v'i'"])],
951 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
952 eval_contains_root "#contains_root_")],
953 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
954 (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
955 (["normalize","univariate","equation","test"],
956 [("#Given" ,["equality e_e","solveFor v_v"]),
958 ("#Find" ,["solutions v_v'i'"])],
959 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
960 (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
961 (["sqroot-test","univariate","equation","test"],
962 [("#Given" ,["equality e_e","solveFor v_v"]),
963 ("#Where" ,["precond_rootpbl v_v"]),
964 ("#Find" ,["solutions v_v'i'"])],
965 e_rls, SOME "solve (e_e::bool, v_v)", [])),
966 (prep_pbt thy "pbl_test_intsimp" [] e_pblID
968 [("#Given" ,["intTestGiven t_t"]),
970 ("#Find" ,["intTestFind s_s"])],
971 e_rls, NONE, [["Test","intsimp"]]))] *}
975 (prep_met thy "met_test_sqrt" [] e_metID
976 (*root-equation, version for tests before 8.01.01*)
977 (["Test","sqrt-equ-test"]:metID,
978 [("#Given" ,["equality e_e","solveFor v_v"]),
979 ("#Where" ,["contains_root (e_e::bool)"]),
980 ("#Find" ,["solutions v_v'i'"])
982 {rew_ord'="e_rew_ord",rls'=tval_rls,
983 srls =append_rls "srls_contains_root" e_rls
984 [Calc ("Test.contains'_root",eval_contains_root "")],
985 prls =append_rls "prls_contains_root" e_rls
986 [Calc ("Test.contains'_root",eval_contains_root "")],
988 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
989 asm_thm=[("square_equation_left",""),
990 ("square_equation_right","")]*)},
991 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
993 " ((While (contains_root e_e) Do" ^
994 " ((Rewrite square_equation_left True) @@" ^
995 " (Try (Rewrite_Set Test_simplify False)) @@" ^
996 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
997 " (Try (Rewrite_Set isolate_root False)) @@" ^
998 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
999 " (Try (Rewrite_Set norm_equation False)) @@" ^
1000 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1001 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1002 " (Try (Rewrite_Set Test_simplify False)))" ^
1010 (prep_met thy "met_test_sqrt2" [] e_metID
1011 (*root-equation ... for test-*.sml until 8.01*)
1012 (["Test","squ-equ-test2"]:metID,
1013 [("#Given" ,["equality e_e","solveFor v_v"]),
1014 ("#Find" ,["solutions v_v'i'"])
1016 {rew_ord'="e_rew_ord",rls'=tval_rls,
1017 srls = append_rls "srls_contains_root" e_rls
1018 [Calc ("Test.contains'_root",eval_contains_root"")],
1020 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1021 asm_thm=[("square_equation_left",""),
1022 ("square_equation_right","")]*)},
1023 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1025 " ((While (contains_root e_e) Do" ^
1026 " ((Rewrite square_equation_left True) @@" ^
1027 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1028 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1029 " (Try (Rewrite_Set isolate_root False)) @@" ^
1030 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1031 " (Try (Rewrite_Set norm_equation False)) @@" ^
1032 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1033 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1034 " (Try (Rewrite_Set Test_simplify False)))" ^
1036 " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
1037 " L_L = Tac solve_equation_dummy " ^
1038 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1044 (prep_met thy "met_test_squ_sub" [] e_metID
1045 (*tests subproblem fixed linear*)
1046 (["Test","squ-equ-test-subpbl1"]:metID,
1047 [("#Given" ,["equality e_e","solveFor v_v"]),
1048 ("#Where" ,["precond_rootmet v_v"]),
1049 ("#Find" ,["solutions v_v'i'"])
1051 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1052 prls = append_rls "prls_met_test_squ_sub" e_rls
1053 [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
1054 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
1055 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1056 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1057 " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1058 " (L_L::bool list) = " ^
1059 " (SubProblem (Test', " ^
1060 " [LINEAR,univariate,equation,test]," ^
1061 " [Test,solve_linear]) " ^
1062 " [BOOL e_e, REAL v_v]) " ^
1063 " in Check_elementwise L_L {(v_v::real). Assumptions}) "
1069 (prep_met thy "met_test_squ_sub2" [] e_metID
1070 (*tests subproblem fixed degree 2*)
1071 (["Test","squ-equ-test-subpbl2"]:metID,
1072 [("#Given" ,["equality e_e","solveFor v_v"]),
1073 ("#Find" ,["solutions v_v'i'"])
1075 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1076 crls=tval_rls, errpats = [], nrls = e_rls(*,
1077 asm_rls=[],asm_thm=[("square_equation_left",""),
1078 ("square_equation_right","")]*)},
1079 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1080 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
1081 "(L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1082 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
1083 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1089 (prep_met thy "met_test_squ_nonterm" [] e_metID
1090 (*root-equation: see foils..., but notTerminating*)
1091 (["Test","square_equation...notTerminating"]:metID,
1092 [("#Given" ,["equality e_e","solveFor v_v"]),
1093 ("#Find" ,["solutions v_v'i'"])
1095 {rew_ord'="e_rew_ord",rls'=tval_rls,
1096 srls = append_rls "srls_contains_root" e_rls
1097 [Calc ("Test.contains'_root",eval_contains_root"")],
1099 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1100 asm_thm=[("square_equation_left",""),
1101 ("square_equation_right","")]*)},
1102 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1104 " ((While (contains_root e_e) Do" ^
1105 " ((Rewrite square_equation_left True) @@" ^
1106 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1107 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1108 " (Try (Rewrite_Set isolate_root False)) @@" ^
1109 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1110 " (Try (Rewrite_Set norm_equation False)) @@" ^
1111 " (Try (Rewrite_Set Test_simplify False)))" ^
1113 " (L_L::bool list) = " ^
1114 " (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1115 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1116 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1122 (prep_met thy "met_test_eq1" [] e_metID
1124 (["Test","square_equation1"]:metID,
1125 [("#Given" ,["equality e_e","solveFor v_v"]),
1126 ("#Find" ,["solutions v_v'i'"])
1128 {rew_ord'="e_rew_ord",rls'=tval_rls,
1129 srls = append_rls "srls_contains_root" e_rls
1130 [Calc ("Test.contains'_root",eval_contains_root"")],
1132 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1133 asm_thm=[("square_equation_left",""),
1134 ("square_equation_right","")]*)},
1135 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1137 " ((While (contains_root e_e) Do" ^
1138 " ((Rewrite square_equation_left True) @@" ^
1139 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1140 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1141 " (Try (Rewrite_Set isolate_root False)) @@" ^
1142 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1143 " (Try (Rewrite_Set norm_equation False)) @@" ^
1144 " (Try (Rewrite_Set Test_simplify False)))" ^
1146 " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
1147 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1148 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1154 (prep_met thy "met_test_squ2" [] e_metID
1156 (["Test","square_equation2"]:metID,
1157 [("#Given" ,["equality e_e","solveFor v_v"]),
1158 ("#Find" ,["solutions v_v'i'"])
1160 {rew_ord'="e_rew_ord",rls'=tval_rls,
1161 srls = append_rls "srls_contains_root" e_rls
1162 [Calc ("Test.contains'_root",eval_contains_root"")],
1164 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1165 asm_thm=[("square_equation_left",""),
1166 ("square_equation_right","")]*)},
1167 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1169 " ((While (contains_root e_e) Do" ^
1170 " (((Rewrite square_equation_left True) Or " ^
1171 " (Rewrite square_equation_right True)) @@" ^
1172 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1173 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1174 " (Try (Rewrite_Set isolate_root False)) @@" ^
1175 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1176 " (Try (Rewrite_Set norm_equation False)) @@" ^
1177 " (Try (Rewrite_Set Test_simplify False)))" ^
1179 " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
1180 " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
1181 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1187 (prep_met thy "met_test_squeq" [] e_metID
1189 (["Test","square_equation"]:metID,
1190 [("#Given" ,["equality e_e","solveFor v_v"]),
1191 ("#Find" ,["solutions v_v'i'"])
1193 {rew_ord'="e_rew_ord",rls'=tval_rls,
1194 srls = append_rls "srls_contains_root" e_rls
1195 [Calc ("Test.contains'_root",eval_contains_root"")],
1197 crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
1198 asm_thm=[("square_equation_left",""),
1199 ("square_equation_right","")]*)},
1200 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1202 " ((While (contains_root e_e) Do" ^
1203 " (((Rewrite square_equation_left True) Or" ^
1204 " (Rewrite square_equation_right True)) @@" ^
1205 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1206 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
1207 " (Try (Rewrite_Set isolate_root False)) @@" ^
1208 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1209 " (Try (Rewrite_Set norm_equation False)) @@" ^
1210 " (Try (Rewrite_Set Test_simplify False)))" ^
1212 " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
1213 " [no_met]) [BOOL e_e, REAL v_v])" ^
1214 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1220 (prep_met thy "met_test_eq_plain" [] e_metID
1221 (*solve_plain_square*)
1222 (["Test","solve_plain_square"]:metID,
1223 [("#Given",["equality e_e","solveFor v_v"]),
1224 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1225 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1226 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1227 "(matches ( v_v ^^^2 = 0) e_e)"]),
1228 ("#Find" ,["solutions v_v'i'"])
1230 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
1231 prls = assoc_rls' @{theory} "matches",
1232 crls=tval_rls, errpats = [], nrls = e_rls(*,
1233 asm_rls=[],asm_thm=[]*)},
1234 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
1235 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
1236 " (Try (Rewrite_Set Test_simplify False)) @@ " ^
1237 " ((Rewrite square_equality_0 False) Or " ^
1238 " (Rewrite square_equality True)) @@ " ^
1239 " (Try (Rewrite_Set tval_rls False))) e_e " ^
1240 " in ((Or_to_List e_e)::bool list))"
1247 (prep_met thy "met_test_norm_univ" [] e_metID
1248 (["Test","norm_univar_equation"]:metID,
1249 [("#Given",["equality e_e","solveFor v_v"]),
1251 ("#Find" ,["solutions v_v'i'"])
1253 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
1255 crls=tval_rls, errpats = [], nrls = e_rls},
1256 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1257 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1258 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1259 " in (SubProblem (Test',[univariate,equation,test], " ^
1260 " [no_met]) [BOOL e_e, REAL v_v]))"
1263 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1266 (prep_met thy "met_test_intsimp" [] e_metID
1267 (["Test","intsimp"]:metID,
1268 [("#Given" ,["intTestGiven t_t"]),
1270 ("#Find" ,["intTestFind s_s"])
1272 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1273 prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
1274 "Script STest_simplify (t_t::int) = " ^
1276 " ((Try (Calculate PLUS)) @@ " ^
1277 " (Try (Calculate TIMES))) t_t::int)"
1283 (*8.4.03 aus Poly.ML--------------------------------vvv---
1284 make_polynomial ---> make_poly
1285 ^-- for user ^-- for systest _ONLY_*)
1287 local (*. for make_polytest .*)
1289 open Term; (* for type order = EQUAL | LESS | GREATER *)
1291 fun pr_ord EQUAL = "EQUAL"
1292 | pr_ord LESS = "LESS"
1293 | pr_ord GREATER = "GREATER";
1295 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1297 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1298 | _ => (((a, 0), T), 0))
1299 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1300 | dest_hd' (Var v) = (v, 2)
1301 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1302 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1304 fun get_order_pow (t $ (Free(order,_))) =
1305 (case int_of_str (order) of
1308 | get_order_pow _ = 0;
1310 fun size_of_term' (Const(str,_) $ t) =
1311 if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
1312 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1313 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1314 | size_of_term' _ = 1;
1315 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1316 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
1318 | term_ord' pr thy (t, u) =
1320 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1321 val _ = tracing ("t= f@ts= \"" ^ term2str f ^ "\" @ \"[" ^
1322 commas(map term2str ts) ^ "]\"")
1323 val _ = tracing ("u= g@us= \"" ^ term2str g ^"\" @ \"[" ^
1324 commas(map term2str us) ^"]\"")
1325 val _ = tracing ("size_of_term(t,u)= (" ^
1326 string_of_int (size_of_term' t) ^ ", " ^
1327 string_of_int (size_of_term' u) ^ ")")
1328 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
1329 val _ = tracing ("terms_ord(ts,us) = " ^
1330 (pr_ord o terms_ord str false) (ts,us));
1331 val _ = tracing "-------"
1334 case int_ord (size_of_term' t, size_of_term' u) of
1336 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1337 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1341 and hd_ord (f, g) = (* ~ term.ML *)
1342 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1343 and terms_ord str pr (ts, us) =
1344 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
1347 fun ord_make_polytest (pr:bool) thy (_:subst) tu =
1348 (term_ord' pr thy(***) tu = LESS );
1354 rew_ord' := overwritel (!rew_ord',
1355 [("termlessI", termlessI),
1356 ("ord_make_polytest", ord_make_polytest false thy)
1359 (*WN060510 this was a preparation for prep_rls ...
1360 val scr_make_polytest =
1361 "Script Expand_binomtest t_t =" ^
1363 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1365 " (Try (Repeat (Rewrite distrib_right False))) @@ " ^
1366 " (Try (Repeat (Rewrite distrib_left False))) @@ " ^
1367 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
1368 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
1370 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1371 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1372 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1374 " (Try (Repeat (Rewrite mult_commute False))) @@ " ^
1375 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
1376 " (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
1377 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
1378 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
1379 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
1381 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1382 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1383 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1384 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1386 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1387 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1389 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1390 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1392 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1393 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1394 " (Try (Repeat (Calculate POWER)))) " ^
1396 -----------------------------------------------------*)
1399 Rls{id = "make_polytest", preconds = []:term list,
1400 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
1401 erls = testerls, srls = Erls,
1402 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1403 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1404 ("POWER", ("Atools.pow", eval_binop "#power_"))
1406 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
1407 (*"a - b = a + (-1) * b"*)
1408 Thm ("distrib_right" ,num_str @{thm distrib_right}),
1409 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1410 Thm ("distrib_left",num_str @{thm distrib_left}),
1411 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1412 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1413 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1414 Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1415 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1416 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1418 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1420 Thm ("add_0_left",num_str @{thm add_0_left}),
1424 Thm ("mult_commute",num_str @{thm mult_commute}),
1426 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1427 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1428 Thm ("mult_assoc",num_str @{thm mult_assoc}),
1429 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1430 Thm ("add_commute",num_str @{thm add_commute}),
1432 Thm ("add_left_commute",num_str @{thm add_left_commute}),
1433 (*x + (y + z) = y + (x + z)*)
1434 Thm ("add_assoc",num_str @{thm add_assoc}),
1435 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1437 Thm ("sym_realpow_twoI",
1438 num_str (@{thm realpow_twoI} RS @{thm sym})),
1439 (*"r1 * r1 = r1 ^^^ 2"*)
1440 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1441 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1442 Thm ("sym_real_mult_2",
1443 num_str (@{thm real_mult_2} RS @{thm sym})),
1444 (*"z1 + z1 = 2 * z1"*)
1445 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1446 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1448 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1449 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1450 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1451 (*"[| l is_const; m is_const |] ==>
1452 l * n + (m * n + k) = (l + m) * n + k"*)
1453 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1454 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1455 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1456 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1458 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1459 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1460 Calc ("Atools.pow", eval_binop "#power_")
1462 scr = EmptyScr(*Prog ((term_of o the o (parse thy))
1463 scr_make_polytest)*)
1467 (*WN060510 this was done before 'fun prep_rls' ...------------------------
1468 val scr_expand_binomtest =
1469 "Script Expand_binomtest t_t =" ^
1471 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
1472 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
1473 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
1474 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
1475 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
1476 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
1478 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1479 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1480 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1482 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1483 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1484 " (Try (Repeat (Calculate POWER))) @@ " ^
1486 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1487 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1488 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1489 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1491 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1492 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1494 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1495 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1497 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1498 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1499 " (Try (Repeat (Calculate POWER)))) " ^
1501 --------------------------------------------------------------------------*)
1503 val expand_binomtest =
1504 Rls{id = "expand_binomtest", preconds = [],
1505 rew_ord = ("termlessI",termlessI),
1506 erls = testerls, srls = Erls,
1507 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1508 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1509 ("POWER", ("Atools.pow", eval_binop "#power_"))
1512 [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
1513 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1514 Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1515 (*"(a + b)*(a + b) = ...*)
1516 Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
1517 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1518 Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
1519 (*"(a - b)*(a - b) = ...*)
1520 Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
1521 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1522 Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
1523 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1525 Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1526 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1527 Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1528 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1529 Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1530 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1531 Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1532 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1533 Thm ("realpow_multI",num_str @{thm realpow_multI}),
1534 (*(a*b)^^^n = a^^^n * b^^^n*)
1535 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1536 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1537 Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
1538 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1541 (* Thm ("distrib_right" ,num_str @{thm distrib_right}),
1542 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1543 Thm ("distrib_left",num_str @{thm distrib_left}),
1544 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1545 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1546 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1547 Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1548 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1551 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1553 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1555 Thm ("add_0_left",num_str @{thm add_0_left}),
1558 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1559 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1560 Calc ("Atools.pow", eval_binop "#power_"),
1562 Thm ("mult_commute",num_str @{thm mult_commute}),
1564 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1565 Thm ("mult_assoc",num_str @{thm mult_assoc}),
1566 Thm ("add_commute",num_str @{thm add_commute}),
1567 Thm ("add_left_commute",num_str @{thm add_left_commute}),
1568 Thm ("add_assoc",num_str @{thm add_assoc}),
1571 Thm ("sym_realpow_twoI",
1572 num_str (@{thm realpow_twoI} RS @{thm sym})),
1573 (*"r1 * r1 = r1 ^^^ 2"*)
1574 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1575 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1576 (*Thm ("sym_real_mult_2",
1577 num_str (@{thm real_mult_2} RS @{thm sym})),
1578 (*"z1 + z1 = 2 * z1"*)*)
1579 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1580 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1582 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1583 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1584 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1585 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1586 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1587 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1588 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1589 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1591 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1592 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1593 Calc ("Atools.pow", eval_binop "#power_")
1596 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
1599 setup {* KEStore_Elems.add_rlss
1600 [("make_polytest", (Context.theory_name @{theory}, prep_rls make_polytest)),
1601 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls expand_binomtest))] *}