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 (_ =))// (_))" 9)
19 bool list] => bool list"
20 ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)
24 bool list] => bool list"
25 ("((Script Solve'_linear (_ _ =))// (_))" 9)
27 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
29 "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
30 "contains'_root" :: "'a => bool" ("contains'_root _" 10)
32 "precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
33 "precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
34 "precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
35 "precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
39 bool list] => bool list"
40 ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)
44 bool list] => bool list"
45 ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)
47 Norm'_univar'_equation
50 ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)
55 ("((Script STest'_simplify (_ =))// (_))" 9)
57 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
59 axiomatization where (*TODO: prove as theorems*)
61 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
62 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
63 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
64 rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
66 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
68 "m is_const ==> (n::real) + m * n = (1 + m) * n" and
69 rcollect_one_left_assoc:
70 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
71 rcollect_one_left_assoc_p:
72 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
74 rtwo_of_the_same: "a + a = 2 * a" and
75 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
76 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
78 rcancel_den: "not(a=0) ==> a * (b / a) = b" and
79 rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
80 rshift_nominator: "(a::real) * b / c = a / c * b" and
82 exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
83 rsqare: "(a::real) * a = a ^^^ 2" and
84 power_1: "(a::real) ^^^ 1 = a" and
85 rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and
87 rmult_1: "1 * k = (k::real)" and
88 rmult_1_right: "k * 1 = (k::real)" and
89 rmult_0: "0 * k = (0::real)" and
90 rmult_0_right: "k * 0 = (0::real)" and
91 radd_0: "0 + k = (k::real)" and
92 radd_0_right: "k + 0 = (k::real)" and
95 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
97 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
100 radd_commute: "(m::real) + (n::real) = n + m" and
101 radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
102 radd_assoc: "(m::real) + n + k = m + (n + k)" and
103 rmult_commute: "(m::real) * n = n * m" and
104 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
105 rmult_assoc: "(m::real) * n * k = m * (n * k)" and
107 (*for equations: 'bdv' is a meta-constant*)
108 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
109 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
110 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
113 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
115 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
116 root_ge0: "0 <= a ==> 0 <= sqrt a" and
117 (*should be dropped with better simplification in eval_rls ...*)
119 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
121 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
126 rroot_square_inv: "(sqrt a)^^^ 2 = a" and
127 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
128 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
129 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
132 (*for root-equations*)
133 square_equation_left:
134 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and
135 square_equation_right:
136 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and
137 (*causes frequently non-termination:*)
139 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and
141 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
142 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
143 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
145 (*for polynomial equations of degree 2; linear case in RatArith*)
146 mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and
147 constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and
148 constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and
151 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
153 "(x^^^2 = 0) = (x = 0)" and
155 (*isolate root on the LEFT hand side of the equation
156 otherwise shuffling from left to right would not terminate*)
159 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
161 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
162 rroot_to_lhs_add_mult:
163 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
164 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
169 (** evaluation of numerals and predicates **)
171 (*does a term contain a root ?*)
172 fun eval_contains_root (thmid:string) _
173 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
174 if member op = (ids_of arg) "sqrt"
175 then SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
176 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
177 else SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
178 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
179 | eval_contains_root _ _ _ _ = NONE;
181 (*dummy precondition for root-met of x+1=2*)
182 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
183 SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg)"",
184 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
185 | eval_precond_rootmet _ _ _ _ = NONE;
187 (*dummy precondition for root-pbl of x+1=2*)
188 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
189 SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
190 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
191 | eval_precond_rootpbl _ _ _ _ = NONE;
193 setup {* KEStore_Elems.add_calcs
194 [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
195 ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
196 ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
197 eval_precond_rootpbl"#Test.precond_rootpbl_"))] *}
200 fun term_order (_: Celem.subst) tu = (term_ordI [] tu = LESS);
205 Celem.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
206 erls = Celem.e_rls, srls = Celem.Erls,
207 calc = [], errpatts = [],
208 rules = [Celem.Thm ("refl",TermC.num_str @{thm refl}),
209 Celem.Thm ("order_refl",TermC.num_str @{thm order_refl}),
210 Celem.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
211 Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
212 Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
213 Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
214 Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
215 Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
216 Celem.Thm ("or_false",TermC.num_str @{thm or_false}),
217 Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}),
218 Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}),
220 Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),
221 Celem.Calc ("Tools.matches",eval_matches ""),
223 Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
224 Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
225 Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
227 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
228 Celem.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
230 Celem.Calc ("Atools.ident",eval_ident "#ident_")],
231 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
235 (*.for evaluation of conditions in rewrite rules.*)
236 (*FIXXXXXXME 10.8.02: handle like _simplify*)
238 Celem.Rls{id = "tval_rls", preconds = [],
239 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
240 erls=testerls,srls = Celem.e_rls,
241 calc=[], errpatts = [],
242 rules = [Celem.Thm ("refl",TermC.num_str @{thm refl}),
243 Celem.Thm ("order_refl",TermC.num_str @{thm order_refl}),
244 Celem.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
245 Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
246 Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
247 Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
248 Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
249 Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
250 Celem.Thm ("or_false",TermC.num_str @{thm or_false}),
251 Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}),
252 Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}),
254 Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
256 Celem.Thm ("root_ge0",TermC.num_str @{thm root_ge0}),
257 Celem.Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}),
258 Celem.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}),
259 Celem.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),
261 Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),
262 Celem.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
263 Celem.Calc ("Tools.matches",eval_matches ""),
264 Celem.Calc ("Test.contains'_root",
265 eval_contains_root"#contains_root_"),
267 Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
268 Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
269 Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
270 Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
272 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
273 Celem.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
275 Celem.Calc ("Atools.ident",eval_ident "#ident_")],
276 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
279 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *}
282 (*make () dissappear*)
283 val rearrange_assoc =
284 Celem.Rls{id = "rearrange_assoc", preconds = [],
285 rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
286 erls = Celem.e_rls, srls = Celem.e_rls, calc = [], errpatts = [],
288 [Celem.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
289 Celem.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
290 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
294 Celem.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
295 erls = Celem.e_rls, srls = Celem.e_rls, calc = [], errpatts = [],
297 [Celem.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
298 Celem.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
299 Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
300 Celem.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
301 Celem.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
302 Celem.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],
303 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
306 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
308 Celem.Rls{id = "norm_equation", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
309 erls = tval_rls, srls = Celem.e_rls, calc = [], errpatts = [],
310 rules = [Celem.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
312 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
318 val STest_simplify = (* vv--- not changed to real by parse*)
319 "Script STest_simplify (t_t::'z) = " ^
321 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
322 " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
323 " (Try (Repeat (Rewrite rdistr_right_assoc False))) @@ " ^
324 " (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^
325 " (Try (Repeat (Rewrite rdistr_div_right False))) @@ " ^
326 " (Try (Repeat (Rewrite rbinom_power_2 False))) @@ " ^
328 " (Try (Repeat (Rewrite radd_commute False))) @@ " ^
329 " (Try (Repeat (Rewrite radd_left_commute False))) @@ " ^
330 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
331 " (Try (Repeat (Rewrite rmult_commute False))) @@ " ^
332 " (Try (Repeat (Rewrite rmult_left_commute False))) @@ " ^
333 " (Try (Repeat (Rewrite rmult_assoc False))) @@ " ^
335 " (Try (Repeat (Rewrite radd_real_const_eq False))) @@ " ^
336 " (Try (Repeat (Rewrite radd_real_const False))) @@ " ^
337 " (Try (Repeat (Calculate PLUS))) @@ " ^
338 " (Try (Repeat (Calculate TIMES))) @@ " ^
339 " (Try (Repeat (Calculate divide_))) @@" ^
340 " (Try (Repeat (Calculate POWER))) @@ " ^
342 " (Try (Repeat (Rewrite rcollect_right False))) @@ " ^
343 " (Try (Repeat (Rewrite rcollect_one_left False))) @@ " ^
344 " (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@ " ^
345 " (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@ " ^
347 " (Try (Repeat (Rewrite rshift_nominator False))) @@ " ^
348 " (Try (Repeat (Rewrite rcancel_den False))) @@ " ^
349 " (Try (Repeat (Rewrite rroot_square_inv False))) @@ " ^
350 " (Try (Repeat (Rewrite rroot_times_root False))) @@ " ^
351 " (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@ " ^
352 " (Try (Repeat (Rewrite rsqare False))) @@ " ^
353 " (Try (Repeat (Rewrite power_1 False))) @@ " ^
354 " (Try (Repeat (Rewrite rtwo_of_the_same False))) @@ " ^
355 " (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@ " ^
357 " (Try (Repeat (Rewrite rmult_1 False))) @@ " ^
358 " (Try (Repeat (Rewrite rmult_1_right False))) @@ " ^
359 " (Try (Repeat (Rewrite rmult_0 False))) @@ " ^
360 " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
361 " (Try (Repeat (Rewrite radd_0 False))) @@ " ^
362 " (Try (Repeat (Rewrite radd_0_right False)))) " ^
367 (* expects * distributed over + *)
369 Celem.Rls{id = "Test_simplify", preconds = [],
370 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
371 erls = tval_rls, srls = Celem.e_rls,
372 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
374 Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
375 Celem.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),
376 Celem.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),
377 Celem.Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}),
378 Celem.Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}),
379 Celem.Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}),
381 Celem.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
382 Celem.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
383 Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
384 Celem.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
385 Celem.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
386 Celem.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}),
388 Celem.Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}),
389 Celem.Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}),
390 (* these 2 rules are invers to distr_div_right wrt. termination.
391 thus they MUST be done IMMEDIATELY before calc *)
392 Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
393 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
394 Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
395 Celem.Calc ("Atools.pow", eval_binop "#power_"),
397 Celem.Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}),
398 Celem.Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}),
399 Celem.Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}),
400 Celem.Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}),
402 Celem.Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}),
403 Celem.Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}),
404 Celem.Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}),
405 Celem.Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}),
406 Celem.Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}),
407 Celem.Thm ("rsqare",TermC.num_str @{thm rsqare}),
408 Celem.Thm ("power_1",TermC.num_str @{thm power_1}),
409 Celem.Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}),
410 Celem.Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}),
412 Celem.Thm ("rmult_1",TermC.num_str @{thm rmult_1}),
413 Celem.Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}),
414 Celem.Thm ("rmult_0",TermC.num_str @{thm rmult_0}),
415 Celem.Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}),
416 Celem.Thm ("radd_0",TermC.num_str @{thm radd_0}),
417 Celem.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})
419 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
420 (*since 040209 filled by prep_rls': STest_simplify*)
429 (*isolate the root in a root-equation*)
431 Celem.Rls{id = "isolate_root", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
432 erls=tval_rls,srls = Celem.e_rls, calc=[], errpatts = [],
433 rules = [Celem.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
434 Celem.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
435 Celem.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),
436 Celem.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),
437 Celem.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),
438 Celem.Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div}) ],
439 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy))
443 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
445 Celem.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
446 erls=tval_rls,srls = Celem.e_rls, calc= [], errpatts = [],
448 [Celem.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
449 Celem.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),
450 Celem.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),
451 Celem.Thm ("mult_square",TermC.num_str @{thm mult_square}),
452 Celem.Thm ("constant_square",TermC.num_str @{thm constant_square}),
453 Celem.Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square})
455 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy))
461 (* association list for calculate_, calculate
462 "Groups.plus_class.plus" etc. not usable in scripts *)
466 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
467 ("matches",("Tools.matches",eval_matches "#matches_")),
468 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
470 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
471 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
472 ("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e")),
473 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
474 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
475 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
476 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
477 ("ident" ,("Atools.ident",eval_ident "#ident_")),
478 (*von hier (ehem.SqRoot*)
479 ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
480 ("Test.contains_root",("contains'_root", eval_contains_root "#contains'_root")),
481 ("Test.contains_root",("contains'_root",
482 eval_contains_root"#contains_root_"))
485 ML {* val prep_rls' = LTool.prep_rls @{theory}; *}
486 setup {* KEStore_Elems.add_rlss
487 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
488 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
489 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
490 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
491 ("matches", (Context.theory_name @{theory}, prep_rls'
492 (Celem.append_rls "matches" testerls [Celem.Calc ("Tools.matches",eval_matches "#matches_")])))] *}
494 (** problem types **)
495 setup {* KEStore_Elems.add_pbts
496 [(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Celem.e_rls, NONE, [])),
497 (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID
498 (["equation","test"],
499 [("#Given" ,["equality e_e","solveFor v_v"]),
500 ("#Where" ,["matches (?a = ?b) e_e"]),
501 ("#Find" ,["solutions v_v'i'"])],
502 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
503 (Specify.prep_pbt thy "pbl_test_uni" [] Celem.e_pblID
504 (["univariate","equation","test"],
505 [("#Given" ,["equality e_e","solveFor v_v"]),
506 ("#Where" ,["matches (?a = ?b) e_e"]),
507 ("#Find" ,["solutions v_v'i'"])],
508 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
509 (Specify.prep_pbt thy "pbl_test_uni_lin" [] Celem.e_pblID
510 (["LINEAR","univariate","equation","test"],
511 [("#Given" ,["equality e_e","solveFor v_v"]),
512 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
513 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
514 ("#Find" ,["solutions v_v'i'"])],
515 assoc_rls' @{theory} "matches",
516 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))(*,
517 (Specify.prep_pbt thy
519 [("#Given" ,"boolTestGiven g_g"),
520 ("#Find" ,"boolTestFind f_f")],
522 (Specify.prep_pbt thy
524 [("#Given" ,"boolTestGiven g_g"),
525 ("#Find" ,"boolTestFind f_f")],
527 (*val ttt = (Thm.term_of o the o (parse (Thy_Info_get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
532 setup {* KEStore_Elems.add_mets
533 [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
535 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
536 crls=Atools_erls, errpats = [], nrls = Celem.e_rls}, "empty_script"),
537 Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
538 (["Test","solve_linear"],
539 [("#Given" ,["equality e_e","solveFor v_v"]),
540 ("#Where" ,["matches (?a = ?b) e_e"]),
541 ("#Find" ,["solutions v_v'i'"])],
542 {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
543 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
544 nrls = Test_simplify},
545 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
548 " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
549 " (Rewrite_Set Test_simplify False))) e_e" ^
550 " in [e_e::bool])")(*,
551 Specify.prep_met thy (*test for equations*)
553 [("#Given" ,["boolTestGiven g_g"]),
554 ("#Find" ,["boolTestFind f_f"])],
555 {rew_ord'="xxxe_rew_ordxxx",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
556 "Script Testeq (e_q::bool) = " ^
558 " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
559 " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
560 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
561 " in e_e) Until (is_root_free e_e)" (*deleted*)) ---------27.4.02*)]
564 setup {* KEStore_Elems.add_rlss
565 [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)),
566 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)),
567 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))] *}
571 fun bin_o (Const (op_,(Type ("fun",
572 [Type (s2,[]),Type ("fun",
573 [Type (s4,tl4),Type (s5,tl5)])])))) =
574 if (s2=s4)andalso(s4=s5)then[op_]else[]
577 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
578 | bin_op t = bin_o t;
579 fun is_bin_op t = ((bin_op t)<>[]);
581 fun bin_op_arg1 ((Const (op_,(Type ("fun",
582 [Type (s2,[]),Type ("fun",
583 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
585 fun bin_op_arg2 ((Const (op_,(Type ("fun",
586 [Type (s2,[]),Type ("fun",
587 [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =
591 exception NO_EQUATION_TERM;
592 fun is_equation ((Const ("HOL.eq",(Type ("fun",
593 [Type (_,[]),Type ("fun",
594 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
596 | is_equation _ = false;
597 fun equ_lhs ((Const ("HOL.eq",(Type ("fun",
598 [Type (_,[]),Type ("fun",
599 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
601 | equ_lhs _ = raise NO_EQUATION_TERM;
602 fun equ_rhs ((Const ("HOL.eq",(Type ("fun",
603 [Type (_,[]),Type ("fun",
604 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
606 | equ_rhs _ = raise NO_EQUATION_TERM;
609 fun atom (Const (_,Type (_,[]))) = true
610 | atom (Free (_,Type (_,[]))) = true
611 | atom (Var (_,Type (_,[]))) = true
612 (*| atom (_ (_,"?DUMMY" )) = true ..ML-error *)
613 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
616 fun varids (Const (s,Type (_,[]))) = [strip_thy s]
617 | varids (Free (s,Type (_,[]))) = if TermC.is_num' s then []
619 | varids (Var((s,_),Type (_,[]))) = [strip_thy s]
620 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
621 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
622 | varids (Abs(a,T,t)) = union op = [a] (varids t)
623 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
625 (*> val t = Thm.term_of (hd (parse Diophant.thy "x"));
626 val t = Free ("x","?DUMMY") : term
628 val it = [] : string list [] !!! *)
631 fun bin_ops_only ((Const op_) $ t1 $ t2) =
632 if(is_bin_op (Const op_))
633 then(bin_ops_only t1)andalso(bin_ops_only t2)
636 if atom t then true else bin_ops_only t;
638 fun polynomial opl t bdVar = (* bdVar TODO *)
639 subset op = (bin_op t, opl) andalso (bin_ops_only t);
641 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
642 andalso polynomial opl (equ_lhs t) bdVar
643 andalso polynomial opl (equ_rhs t) bdVar
644 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
645 subset op = (varids bdVar, varids (equ_lhs t)));
648 let fun max_ m [] = m
649 | max_ m (i::is) = if m<i then max_ i is else max_ m is;
650 in max_ (hd is) is end;
654 fun max (a,b) = if a < b then b else a;
656 fun degree addl mul bdVar t =
658 fun deg _ _ v (Const (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
659 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0
660 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0
661 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
662 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0
663 | deg addl mul v (h $ t1 $ t2) =
664 if subset op = (bin_op h, addl)
665 then max (deg addl mul v t1 ,deg addl mul v t2)
666 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
667 in if polynomial (addl @ [mul]) t bdVar
668 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)
670 fun degree_ addl mul bdVar t = (* do not export *)
671 let fun opt (SOME i)= i
673 in opt (degree addl mul bdVar t) end;
676 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;
678 fun linear_equ addl mul bdVar t =
680 then let val degl = degree_ addl mul bdVar (equ_lhs t);
681 val degr = degree_ addl mul bdVar (equ_rhs t)
682 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2
686 (* strip_thy op_ before *)
687 fun is_div_op (dv,(Const (op_,(Type ("fun",
688 [Type (s2,[]),Type ("fun",
689 [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)
690 | is_div_op _ = false;
692 fun is_denom bdVar div_op t =
693 let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
694 | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
695 | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
696 | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
697 | is bool[v]dv (h$n$d) =
699 then (is false[v]dv n)orelse(is true[v]dv d)
700 else (is bool [v]dv n)orelse(is bool[v]dv d)
701 in is false (varids bdVar) (strip_thy div_op) t end;
704 fun rational t div_op bdVar =
705 is_denom bdVar div_op t andalso bin_ops_only t;
708 (** problem types **)
709 setup {* KEStore_Elems.add_pbts
710 [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Celem.e_pblID
711 (["plain_square","univariate","equation","test"],
712 [("#Given" ,["equality e_e","solveFor v_v"]),
713 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
714 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
715 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
716 "(matches ( v_v ^^^2 = 0) e_e)"]),
717 ("#Find" ,["solutions v_v'i'"])],
718 assoc_rls' @{theory} "matches",
719 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
721 val e_e = (Thm.term_of o the o (parse thy)) "e_e::bool";
722 val ve = (Thm.term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
725 val pre = (Thm.term_of o the o (parse thy))
726 "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
727 "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
728 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
729 "(matches ( v_v ^^^2 = 0, e_e::bool))";
730 val prei = subst_atomic env pre;
731 val cpre = (Thm.global_cterm_of thy) prei;
733 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
734 val ct = "True | False | False | False" : cterm
736 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
737 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
738 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
739 val ct = "HOL.True" : cterm
742 setup {* KEStore_Elems.add_pbts
743 [(Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID
744 (["polynomial","univariate","equation","test"],
745 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
746 ("#Where" ,["HOL.False"]),
747 ("#Find" ,["solutions v_v'i'"])],
748 Celem.e_rls, SOME "solve (e_e::bool, v_v)", [])),
749 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID
750 (["degree_two","polynomial","univariate","equation","test"],
751 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
752 ("#Find" ,["solutions v_v'i'"])],
753 Celem.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
754 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID
755 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
756 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
757 ("#Find" ,["solutions v_v'i'"])],
758 Celem.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
759 (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID
760 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
761 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
762 ("#Find" ,["solutions v_v'i'"])],
763 Celem.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
764 (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID
765 (["squareroot","univariate","equation","test"],
766 [("#Given" ,["equality e_e","solveFor v_v"]),
767 ("#Where" ,["precond_rootpbl v_v"]),
768 ("#Find" ,["solutions v_v'i'"])],
769 Celem.append_rls "contains_root" Celem.e_rls [Celem.Calc ("Test.contains'_root",
770 eval_contains_root "#contains_root_")],
771 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
772 (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID
773 (["normalise","univariate","equation","test"],
774 [("#Given" ,["equality e_e","solveFor v_v"]),
776 ("#Find" ,["solutions v_v'i'"])],
777 Celem.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
778 (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID
779 (["sqroot-test","univariate","equation","test"],
780 [("#Given" ,["equality e_e","solveFor v_v"]),
781 ("#Where" ,["precond_rootpbl v_v"]),
782 ("#Find" ,["solutions v_v'i'"])],
783 Celem.e_rls, SOME "solve (e_e::bool, v_v)", [])),
784 (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID
786 [("#Given" ,["intTestGiven t_t"]),
788 ("#Find" ,["intTestFind s_s"])],
789 Celem.e_rls, NONE, [["Test","intsimp"]]))] *}
792 get_pbt ["inttype","test"];
795 setup {* KEStore_Elems.add_mets
796 [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID
797 (*root-equation, version for tests before 8.01.01*)
798 (["Test","sqrt-equ-test"],
799 [("#Given" ,["equality e_e","solveFor v_v"]),
800 ("#Where" ,["contains_root (e_e::bool)"]),
801 ("#Find" ,["solutions v_v'i'"])],
802 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
803 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
804 [Celem.Calc ("Test.contains'_root",eval_contains_root "")],
805 prls = Celem.append_rls "prls_contains_root" Celem.e_rls
806 [Celem.Calc ("Test.contains'_root",eval_contains_root "")],
807 calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls (*,asm_rls=[],
808 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
809 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
811 " ((While (contains_root e_e) Do" ^
812 " ((Rewrite square_equation_left True) @@" ^
813 " (Try (Rewrite_Set Test_simplify False)) @@" ^
814 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
815 " (Try (Rewrite_Set isolate_root False)) @@" ^
816 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
817 " (Try (Rewrite_Set norm_equation False)) @@" ^
818 " (Try (Rewrite_Set Test_simplify False)) @@" ^
819 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
820 " (Try (Rewrite_Set Test_simplify False)))" ^
823 Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID
824 (*root-equation ... for test-*.sml until 8.01*)
825 (["Test","squ-equ-test2"],
826 [("#Given" ,["equality e_e","solveFor v_v"]),
827 ("#Find" ,["solutions v_v'i'"])],
828 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
829 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
830 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
831 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
832 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
833 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
835 " ((While (contains_root e_e) Do" ^
836 " ((Rewrite square_equation_left True) @@" ^
837 " (Try (Rewrite_Set Test_simplify False)) @@" ^
838 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
839 " (Try (Rewrite_Set isolate_root False)) @@" ^
840 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
841 " (Try (Rewrite_Set norm_equation False)) @@" ^
842 " (Try (Rewrite_Set Test_simplify False)) @@" ^
843 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
844 " (Try (Rewrite_Set Test_simplify False)))" ^
846 " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
847 " L_L = Tac solve_equation_dummy " ^
848 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
849 Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
850 (*tests subproblem fixed linear*)
851 (["Test","squ-equ-test-subpbl1"],
852 [("#Given" ,["equality e_e","solveFor v_v"]),
853 ("#Where" ,["precond_rootmet v_v"]),
854 ("#Find" ,["solutions v_v'i'"])],
855 {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
856 prls = Celem.append_rls "prls_met_test_squ_sub" Celem.e_rls
857 [Celem.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
858 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
859 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
860 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
861 " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
862 " (L_L::bool list) = " ^
863 " (SubProblem (Test', " ^
864 " [LINEAR,univariate,equation,test]," ^
865 " [Test,solve_linear]) " ^
866 " [BOOL e_e, REAL v_v]) " ^
867 " in Check_elementwise L_L {(v_v::real). Assumptions}) "),
868 Specify.prep_met thy "met_test_squ_sub2" [] Celem.e_metID
869 (*tests subproblem fixed degree 2*)
870 (["Test","squ-equ-test-subpbl2"],
871 [("#Given" ,["equality e_e","solveFor v_v"]),
872 ("#Find" ,["solutions v_v'i'"])],
873 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls=Celem.e_rls,prls=Celem.e_rls,calc=[], crls=tval_rls,
874 errpats = [], nrls = Celem.e_rls (*, asm_rls=[],asm_thm=[("square_equation_left",""),
875 ("square_equation_right","")]*)},
876 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
877 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
878 "(L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
879 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
880 "in Check_elementwise L_L {(v_v::real). Assumptions})"),
881 Specify.prep_met thy "met_test_squ_nonterm" [] Celem.e_metID
882 (*root-equation: see foils..., but notTerminating*)
883 (["Test","square_equation...notTerminating"],
884 [("#Given" ,["equality e_e","solveFor v_v"]),
885 ("#Find" ,["solutions v_v'i'"])],
886 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
887 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
888 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
889 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
890 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
891 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
893 " ((While (contains_root e_e) Do" ^
894 " ((Rewrite square_equation_left True) @@" ^
895 " (Try (Rewrite_Set Test_simplify False)) @@" ^
896 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
897 " (Try (Rewrite_Set isolate_root False)) @@" ^
898 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
899 " (Try (Rewrite_Set norm_equation False)) @@" ^
900 " (Try (Rewrite_Set Test_simplify False)))" ^
902 " (L_L::bool list) = " ^
903 " (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
904 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
905 "in Check_elementwise L_L {(v_v::real). Assumptions})"),
906 Specify.prep_met thy "met_test_eq1" [] Celem.e_metID
908 (["Test","square_equation1"],
909 [("#Given" ,["equality e_e","solveFor v_v"]),
910 ("#Find" ,["solutions v_v'i'"])],
911 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
912 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
913 [Celem.Calc ("Test.contains'_root",eval_contains_root"")], prls=Celem.e_rls, calc=[], crls=tval_rls,
914 errpats = [], nrls = Celem.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
915 ("square_equation_right","")]*)},
916 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
918 " ((While (contains_root e_e) Do" ^
919 " ((Rewrite square_equation_left True) @@" ^
920 " (Try (Rewrite_Set Test_simplify False)) @@" ^
921 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
922 " (Try (Rewrite_Set isolate_root False)) @@" ^
923 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
924 " (Try (Rewrite_Set norm_equation False)) @@" ^
925 " (Try (Rewrite_Set Test_simplify False)))" ^
927 " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
928 " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
929 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
930 Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
932 (["Test","square_equation2"],
933 [("#Given" ,["equality e_e","solveFor v_v"]),
934 ("#Find" ,["solutions v_v'i'"])],
935 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
936 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
937 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
938 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
939 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
940 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
942 " ((While (contains_root e_e) Do" ^
943 " (((Rewrite square_equation_left True) Or " ^
944 " (Rewrite square_equation_right True)) @@" ^
945 " (Try (Rewrite_Set Test_simplify False)) @@" ^
946 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
947 " (Try (Rewrite_Set isolate_root False)) @@" ^
948 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
949 " (Try (Rewrite_Set norm_equation False)) @@" ^
950 " (Try (Rewrite_Set Test_simplify False)))" ^
952 " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
953 " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
954 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
955 Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
957 (["Test","square_equation"],
958 [("#Given" ,["equality e_e","solveFor v_v"]),
959 ("#Find" ,["solutions v_v'i'"])],
960 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
961 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
962 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
963 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls (*,asm_rls=[],
964 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
965 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
967 " ((While (contains_root e_e) Do" ^
968 " (((Rewrite square_equation_left True) Or" ^
969 " (Rewrite square_equation_right True)) @@" ^
970 " (Try (Rewrite_Set Test_simplify False)) @@" ^
971 " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
972 " (Try (Rewrite_Set isolate_root False)) @@" ^
973 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
974 " (Try (Rewrite_Set norm_equation False)) @@" ^
975 " (Try (Rewrite_Set Test_simplify False)))" ^
977 " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
978 " [no_met]) [BOOL e_e, REAL v_v])" ^
979 " in Check_elementwise L_L {(v_v::real). Assumptions})"),
980 Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
981 (*solve_plain_square*)
982 (["Test","solve_plain_square"],
983 [("#Given",["equality e_e","solveFor v_v"]),
984 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
985 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
986 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
987 "(matches ( v_v ^^^2 = 0) e_e)"]),
988 ("#Find" ,["solutions v_v'i'"])],
989 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,calc=[],srls=Celem.e_rls,
990 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,
991 asm_rls=[],asm_thm=[]*)},
992 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
993 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
994 " (Try (Rewrite_Set Test_simplify False)) @@ " ^
995 " ((Rewrite square_equality_0 False) Or " ^
996 " (Rewrite square_equality True)) @@ " ^
997 " (Try (Rewrite_Set tval_rls False))) e_e " ^
998 " in ((Or_to_List e_e)::bool list))"),
999 Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
1000 (["Test","norm_univar_equation"],
1001 [("#Given",["equality e_e","solveFor v_v"]),
1003 ("#Find" ,["solutions v_v'i'"])],
1004 {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls = Celem.e_rls,prls=Celem.e_rls, calc=[], crls=tval_rls,
1005 errpats = [], nrls = Celem.e_rls},
1006 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1007 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1008 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1009 " in (SubProblem (Test',[univariate,equation,test], " ^
1010 " [no_met]) [BOOL e_e, REAL v_v]))"),
1011 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1012 Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
1013 (["Test","intsimp"],
1014 [("#Given" ,["intTestGiven t_t"]),
1016 ("#Find" ,["intTestFind s_s"])],
1017 {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
1018 crls = tval_rls, errpats = [], nrls = Test_simplify},
1019 "Script STest_simplify (t_t::int) = " ^
1021 " ((Try (Calculate PLUS)) @@ " ^
1022 " (Try (Calculate TIMES))) t_t::int)")]
1026 (*8.4.03 aus Poly.ML--------------------------------vvv---
1027 make_polynomial ---> make_poly
1028 ^-- for user ^-- for systest _ONLY_*)
1030 local (*. for make_polytest .*)
1032 open Term; (* for type order = EQUAL | LESS | GREATER *)
1034 fun pr_ord EQUAL = "EQUAL"
1035 | pr_ord LESS = "LESS"
1036 | pr_ord GREATER = "GREATER";
1038 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1040 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1041 | _ => (((a, 0), T), 0))
1042 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1043 | dest_hd' (Var v) = (v, 2)
1044 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1045 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1047 fun get_order_pow (t $ (Free(order,_))) =
1048 (case TermC.int_of_str_opt (order) of
1051 | get_order_pow _ = 0;
1053 fun size_of_term' (Const(str,_) $ t) =
1054 if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
1055 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1056 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1057 | size_of_term' _ = 1;
1058 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1059 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
1061 | term_ord' pr thy (t, u) =
1063 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1064 val _ = tracing ("t= f@ts= \"" ^ Celem.term2str f ^ "\" @ \"[" ^
1065 commas(map Celem.term2str ts) ^ "]\"")
1066 val _ = tracing ("u= g@us= \"" ^ Celem.term2str g ^"\" @ \"[" ^
1067 commas(map Celem.term2str us) ^"]\"")
1068 val _ = tracing ("size_of_term(t,u)= (" ^
1069 string_of_int (size_of_term' t) ^ ", " ^
1070 string_of_int (size_of_term' u) ^ ")")
1071 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
1072 val _ = tracing ("terms_ord(ts,us) = " ^
1073 (pr_ord o terms_ord str false) (ts,us));
1074 val _ = tracing "-------"
1077 case int_ord (size_of_term' t, size_of_term' u) of
1079 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1080 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1084 and hd_ord (f, g) = (* ~ term.ML *)
1085 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1086 and terms_ord str pr (ts, us) =
1087 list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
1090 fun ord_make_polytest (pr:bool) thy (_: Celem.subst) tu =
1091 (term_ord' pr thy(***) tu = LESS );
1097 Celem.rew_ord' := overwritel (! Celem.rew_ord',
1098 [("termlessI", termlessI),
1099 ("ord_make_polytest", ord_make_polytest false thy)
1102 (*WN060510 this was a preparation for prep_rls' ...
1103 val scr_make_polytest =
1104 "Script Expand_binomtest t_t =" ^
1106 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1108 " (Try (Repeat (Rewrite distrib_right False))) @@ " ^
1109 " (Try (Repeat (Rewrite distrib_left False))) @@ " ^
1110 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
1111 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
1113 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1114 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1115 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1117 " (Try (Repeat (Rewrite mult_commute False))) @@ " ^
1118 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
1119 " (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
1120 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
1121 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
1122 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
1124 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1125 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1126 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1127 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1129 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1130 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1132 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1133 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1135 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1136 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1137 " (Try (Repeat (Calculate POWER)))) " ^
1139 -----------------------------------------------------*)
1142 Celem.Rls{id = "make_polytest", preconds = []:term list,
1143 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
1144 erls = testerls, srls = Celem.Erls,
1145 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1146 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1147 ("POWER", ("Atools.pow", eval_binop "#power_"))
1149 rules = [Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1150 (*"a - b = a + (-1) * b"*)
1151 Celem.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1152 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1153 Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1154 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1155 Celem.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1156 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1157 Celem.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1158 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1159 Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1161 Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1163 Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1167 Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1169 Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1170 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1171 Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1172 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1173 Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1175 Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1176 (*x + (y + z) = y + (x + z)*)
1177 Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1178 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1180 Celem.Thm ("sym_realpow_twoI",
1181 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1182 (*"r1 * r1 = r1 ^^^ 2"*)
1183 Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1184 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1185 Celem.Thm ("sym_real_mult_2",
1186 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1187 (*"z1 + z1 = 2 * z1"*)
1188 Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1189 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1191 Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1192 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1193 Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1194 (*"[| l is_const; m is_const |] ==>
1195 l * n + (m * n + k) = (l + m) * n + k"*)
1196 Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1197 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1198 Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1199 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1201 Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1202 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1203 Celem.Calc ("Atools.pow", eval_binop "#power_")
1205 scr = Celem.EmptyScr(*Celem.Prog ((Thm.term_of o the o (parse thy))
1206 scr_make_polytest)*)
1210 (*WN060510 this was done before 'fun prep_rls ...------------------------
1211 val scr_expand_binomtest =
1212 "Script Expand_binomtest t_t =" ^
1214 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
1215 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
1216 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
1217 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
1218 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
1219 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
1221 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1222 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1223 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1225 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1226 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1227 " (Try (Repeat (Calculate POWER))) @@ " ^
1229 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1230 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1231 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1232 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1234 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1235 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1237 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1238 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1240 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1241 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1242 " (Try (Repeat (Calculate POWER)))) " ^
1244 --------------------------------------------------------------------------*)
1246 val expand_binomtest =
1247 Celem.Rls{id = "expand_binomtest", preconds = [],
1248 rew_ord = ("termlessI",termlessI),
1249 erls = testerls, srls = Celem.Erls,
1250 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1251 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1252 ("POWER", ("Atools.pow", eval_binop "#power_"))
1255 [Celem.Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}),
1256 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1257 Celem.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1258 (*"(a + b)*(a + b) = ...*)
1259 Celem.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),
1260 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1261 Celem.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),
1262 (*"(a - b)*(a - b) = ...*)
1263 Celem.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),
1264 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1265 Celem.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),
1266 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1268 Celem.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
1269 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1270 Celem.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
1271 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1272 Celem.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
1273 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1274 Celem.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
1275 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1276 Celem.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1277 (*(a*b)^^^n = a^^^n * b^^^n*)
1278 Celem.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
1279 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1280 Celem.Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}),
1281 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1284 (* Celem.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1285 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1286 Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1287 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1288 Celem.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1289 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1290 Celem.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1291 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1294 Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1296 Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1298 Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1301 Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1302 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1303 Celem.Calc ("Atools.pow", eval_binop "#power_"),
1305 Celem.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1307 Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1308 Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1309 Celem.Thm ("add_commute",TermC.num_str @{thm add_commute}),
1310 Celem.Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}),
1311 Celem.Thm ("add_assoc",TermC.num_str @{thm add_assoc}),
1314 Celem.Thm ("sym_realpow_twoI",
1315 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1316 (*"r1 * r1 = r1 ^^^ 2"*)
1317 Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1318 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1319 (*Celem.Thm ("sym_real_mult_2",
1320 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1321 (*"z1 + z1 = 2 * z1"*)*)
1322 Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1323 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1325 Celem.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1326 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1327 Celem.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1328 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1329 Celem.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1330 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1331 Celem.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1332 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1334 Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1335 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1336 Celem.Calc ("Atools.pow", eval_binop "#power_")
1338 scr = Celem.EmptyScr
1339 (*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
1342 setup {* KEStore_Elems.add_rlss
1343 [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)),
1344 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))] *}