1 (* tools for arithmetic
3 use"../Knowledge/Atools.ML";
4 use"Knowledge/Atools.ML";
9 copy from doc/math-eng.tex WN.28.3.03
12 \section{Coding standards}
14 %WN071228 extended -----vvv
15 \subsection{Identifiers}
16 Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
18 This are the preliminary rules for naming identifiers>
20 \item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
21 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
22 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
23 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
27 %WN071228 extended -----^^^
30 \subsection{Rule sets}
31 The actual version of the coding standards for rulesets is in {\tt /Knowledge/Atools.ML where it can be viewed using the knowledge browsers.
33 There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
36 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents).
38 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student.
40 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only.
41 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise).
44 The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
45 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
53 {\tt append_rls, merge_rls, remove_rls}
56 "******* Atools.ML begin *******";
57 theory' := overwritel (!theory', [("Atools.thy",Atools.thy)]);
59 (** evaluation of numerals and special predicates on the meta-level **)
60 (*-------------------------functions---------------------*)
61 local (* rlang 09.02 *)
62 (*.a 'c is coefficient of v' if v does occur in c.*)
63 fun coeff_in v c = member op = (vars c) v;
65 fun occurs_in v t = coeff_in v t;
68 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
69 fun eval_occurs_in _ "Atools.occurs'_in"
70 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
71 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
72 writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
74 then SOME ((term2str p) ^ " = True",
75 Trueprop $ (mk_equality (p, HOLogic.true_const)))
76 else SOME ((term2str p) ^ " = False",
77 Trueprop $ (mk_equality (p, HOLogic.false_const))))
78 | eval_occurs_in _ _ _ _ = NONE;
80 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
81 fun some_occur_in vs t =
82 let fun occurs_in' a b = occurs_in b a
83 in foldl or_ (false, map (occurs_in' t) vs) end;
85 (*("some_occur_in", ("Atools.some'_occur'_in",
86 eval_some_occur_in "#eval_some_occur_in_"))*)
87 fun eval_some_occur_in _ "Atools.some'_occur'_in"
88 (p as (Const ("Atools.some'_occur'_in",_)
90 if some_occur_in (isalist2list vs) t
91 then SOME ((term2str p) ^ " = True",
92 Trueprop $ (mk_equality (p, HOLogic.true_const)))
93 else SOME ((term2str p) ^ " = False",
94 Trueprop $ (mk_equality (p, HOLogic.false_const)))
95 | eval_some_occur_in _ _ _ _ = NONE;
100 (*evaluate 'is_atom'*)
101 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
102 fun eval_is_atom (thmid:string) "Atools.is'_atom"
103 (t as (Const(op0,_) $ arg)) thy =
105 Free (n,_) => SOME (mk_thmid thmid op0 n "",
106 Trueprop $ (mk_equality (t, true_as_term)))
107 | _ => SOME (mk_thmid thmid op0 "" "",
108 Trueprop $ (mk_equality (t, false_as_term))))
109 | eval_is_atom _ _ _ _ = NONE;
111 (*evaluate 'is_even'*)
112 fun even i = (i div 2) * 2 = i;
113 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
114 fun eval_is_even (thmid:string) "Atools.is'_even"
115 (t as (Const(op0,_) $ arg)) thy =
118 (case int_of_str n of
120 if even i then SOME (mk_thmid thmid op0 n "",
121 Trueprop $ (mk_equality (t, true_as_term)))
122 else SOME (mk_thmid thmid op0 "" "",
123 Trueprop $ (mk_equality (t, false_as_term)))
126 | eval_is_even _ _ _ _ = NONE;
128 (*evaluate 'is_const'*)
129 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
130 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
131 (t as (Const(op0,t0) $ arg)) (thy:theory) =
132 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
135 SOME (mk_thmid thmid op0 n1 "",
136 Trueprop $ (mk_equality (t, false_as_term)))
139 then SOME (mk_thmid thmid op0 n1 "",
140 Trueprop $ (mk_equality (t, true_as_term)))
141 else SOME (mk_thmid thmid op0 n1 "",
142 Trueprop $ (mk_equality (t, false_as_term)))
143 | Const ("Float.Float",_) =>
144 SOME (mk_thmid thmid op0 (term2str arg) "",
145 Trueprop $ (mk_equality (t, true_as_term)))
147 SOME (mk_thmid thmid op0 (term2str arg) "",
148 Trueprop $ (mk_equality (t, false_as_term))))
149 | eval_const _ _ _ _ = NONE;
151 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
152 (*("PLUS" ,("op +" ,eval_binop "#add_")),
153 ("TIMES" ,("op *" ,eval_binop "#mult_")),
154 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
156 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
157 ("xxxxxx",op_,t,thy);
159 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
161 (string_of_int v11)^","^(string_of_int v12)^"), ("^
162 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
163 (string_of_int v21)^","^(string_of_int v22)^"), ("^
164 (string_of_int p21)^","^(string_of_int p22)^"))";
166 (*.convert int and float to internal floatingpoint prepresentation.*)
167 fun numeral (Free (str, T)) =
168 (case int_of_str str of
169 SOME i => SOME ((i, 0), (0, 0))
171 | numeral (Const ("Float.Float", _) $
173 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
174 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
175 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
176 (SOME v1', SOME v2', SOME p1', SOME p2') =>
177 SOME ((v1', v2'), (p1', p2'))
181 (*.evaluate binary associative operations.*)
182 fun eval_binop (thmid:string) (op_:string)
183 (t as ( Const(op0,t0) $
184 (Const(op0',t0') $ v $ t1) $ t2))
185 thy = (*binary . (v.n1).n2*)
187 case (numeral t1, numeral t2) of
188 (SOME n1, SOME n2) =>
189 let val (T1,T2,Trange) = dest_binop_typ t0
190 val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
191 (*WN071229 "HOL.divide" never tried*)
192 val rhs = var_op_float v op_ t0 T1 res
193 val prop = Trueprop $ (mk_equality (t, rhs))
194 in SOME (mk_thmid_f thmid n1 n2, prop) end
197 | eval_binop (thmid:string) (op_:string)
199 (Const (op0, t0) $ t1 $
200 (Const (op0', t0') $ t2 $ v)))
201 thy = (*binary . n1.(n2.v)*)
203 case (numeral t1, numeral t2) of
204 (SOME n1, SOME n2) =>
205 if op0 = "op -" then NONE else
206 let val (T1,T2,Trange) = dest_binop_typ t0
207 val res = calc op0 n1 n2
208 val rhs = float_op_var v op_ t0 T1 res
209 val prop = Trueprop $ (mk_equality (t, rhs))
210 in SOME (mk_thmid_f thmid n1 n2, prop) end
214 | eval_binop (thmid:string) (op_:string)
215 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
216 (case (numeral t1, numeral t2) of
217 (SOME n1, SOME n2) =>
218 let val (T1,T2,Trange) = dest_binop_typ t0;
219 val res = calc op0 n1 n2;
220 val rhs = term_of_float Trange res;
221 val prop = Trueprop $ (mk_equality (t, rhs));
222 in SOME (mk_thmid_f thmid n1 n2, prop) end
224 | eval_binop _ _ _ _ = NONE;
226 > val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
228 val it = "-1 + 2 = 1"
229 > val t = str2term "-1 * (-1 * a)";
230 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
232 val it = "-1 * (-1 * a) = 1 * a"*)
236 (*.evaluate < and <= for numerals.*)
237 (*("le" ,("op <" ,eval_equ "#less_")),
238 ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
239 fun eval_equ (thmid:string) (op_:string) (t as
240 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
241 (case (int_of_str n1, int_of_str n2) of
242 (SOME n1', SOME n2') =>
243 if calc_equ (strip_thy op0) (n1', n2')
244 then SOME (mk_thmid thmid op0 n1 n2,
245 Trueprop $ (mk_equality (t, true_as_term)))
246 else SOME (mk_thmid thmid op0 n1 n2,
247 Trueprop $ (mk_equality (t, false_as_term)))
250 | eval_equ _ _ _ _ = NONE;
255 val it = "(?t = ?t) = True"
256 > val t = str2term "x = 0";
257 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
259 > val t = str2term "1 = 0";
260 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
261 ----------- thus needs Calc !
262 > val t = str2term "0 = 0";
263 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
267 val t = str2term "Not (x = 0)";
274 val it = "x ~= 0" : string*)
276 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
277 the arguments: thus special handling by 'fun eval_binop'*)
278 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
279 fun eval_ident (thmid:string) "Atools.ident" (t as
280 (Const (op0,t0) $ t1 $ t2 )) thy =
282 then SOME (mk_thmid thmid op0
283 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
284 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
285 Trueprop $ (mk_equality (t, true_as_term)))
286 else SOME (mk_thmid thmid op0
287 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
288 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
289 Trueprop $ (mk_equality (t, false_as_term)))
290 | eval_ident _ _ _ _ = NONE;
292 > val t = str2term "x =!= 0";
293 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
295 val str = "ident_(x)_(0)" : string
296 val it = "(x =!= 0) = False" : string
297 > val t = str2term "1 =!= 0";
298 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
300 val str = "ident_(1)_(0)" : string
301 val it = "(1 =!= 0) = False" : string
302 > val t = str2term "0 =!= 0";
303 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
305 val str = "ident_(0)_(0)" : string
306 val it = "(0 =!= 0) = True" : string
309 (*.evaluate identity of terms, which stay ready for evaluation in turn;
310 thus returns False only for atoms.*)
311 (*("equal" ,("op =",eval_equal "#equal_")):calc*)
312 fun eval_equal (thmid:string) "op =" (t as
313 (Const (op0,t0) $ t1 $ t2 )) thy =
315 then ((*writeln"... eval_equal: t1 = t2 --> True";*)
316 SOME (mk_thmid thmid op0
317 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
318 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
319 Trueprop $ (mk_equality (t, true_as_term)))
321 else (case (is_atom t1, is_atom t2) of
323 ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
324 SOME (mk_thmid thmid op0
325 ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
326 Trueprop $ (mk_equality (t, false_as_term)))
328 | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
330 | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
333 val t = str2term "x ~= 0";
334 val NONE = eval_equal "equal_" "b" t thy;
337 > val t = str2term "(x + 1) = (x + 1)";
338 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
340 val str = "equal_(x + 1)_(x + 1)" : string
341 val it = "(x + 1 = x + 1) = True" : string
342 > val t = str2term "x = 0";
343 > val NONE = eval_equal "equal_" "b" t thy;
345 > val t = str2term "1 = 0";
346 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
348 val str = "equal_(1)_(0)" : string
349 val it = "(1 = 0) = False" : string
350 > val t = str2term "0 = 0";
351 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
353 val str = "equal_(0)_(0)" : string
354 val it = "(0 = 0) = True" : string
358 (** evaluation on the metalevel **)
360 (*. evaluate HOL.divide .*)
361 (*("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_"))*)
362 fun eval_cancel (thmid:string) "HOL.divide" (t as
363 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
364 (case (int_of_str n1, int_of_str n2) of
365 (SOME n1', SOME n2') =>
367 val sg = sign2 n1' n2';
368 val (T1,T2,Trange) = dest_binop_typ t0;
369 val gcd' = gcd (abs n1') (abs n2');
371 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
372 val prop = Trueprop $ (mk_equality (t, rhs))
373 in SOME (mk_thmid thmid op0 n1 n2, prop) end
374 else if 0 < n2' andalso gcd' = 1 then NONE
375 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
377 val prop = Trueprop $ (mk_equality (t, rhs))
378 in SOME (mk_thmid thmid op0 n1 n2, prop) end
380 | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
382 | eval_cancel _ _ _ _ = NONE;
384 (*. get the argument from a function-definition.*)
385 (*("argument_in" ,("Atools.argument'_in",
386 eval_argument_in "Atools.argument'_in"))*)
387 fun eval_argument_in _ "Atools.argument'_in"
388 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
389 if is_Free arg (*could be something to be simplified before*)
390 then SOME (term2str t ^ " = " ^ term2str arg,
391 Trueprop $ (mk_equality (t, arg)))
393 | eval_argument_in _ _ _ _ = NONE;
395 (*.check if the function-identifier of the first argument matches
396 the function-identifier of the lhs of the second argument.*)
397 (*("sameFunId" ,("Atools.sameFunId",
398 eval_same_funid "Atools.sameFunId"))*)
399 fun eval_sameFunId _ "Atools.sameFunId"
400 (p as Const ("Atools.sameFunId",_) $
402 (Const ("op =", _) $ (f2 $ _) $ _)) _ =
404 then SOME ((term2str p) ^ " = True",
405 Trueprop $ (mk_equality (p, HOLogic.true_const)))
406 else SOME ((term2str p) ^ " = False",
407 Trueprop $ (mk_equality (p, HOLogic.false_const)))
408 | eval_sameFunId _ _ _ _ = NONE;
411 (*.from a list of fun-definitions "f x = ..." as 2nd argument
412 filter the elements with the same fun-identfier in "f y"
414 this is, because Isabelles filter takes more than 1 sec.*)
415 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
416 | same_funid f1 t = raise error ("same_funid called with t = ("
417 ^term2str f1^") ("^term2str t^")");
418 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
419 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
420 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
421 (p as Const ("Atools.filter'_sameFunId",_) $
423 let val fs' = ((list2isalist HOLogic.boolT) o
424 (filter (same_funid fid))) (isalist2list fs)
425 in SOME (term2str (mk_equality (p, fs')),
426 Trueprop $ (mk_equality (p, fs'))) end
427 | eval_filter_sameFunId _ _ _ _ = NONE;
430 (*make a list of terms to a sum*)
431 fun list2sum [] = error ("list2sum called with []")
434 let fun sum su [s'] =
435 Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
438 sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
442 (*make a list of equalities to the sum of the lhs*)
443 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
444 fun eval_boollist2sum _ "Atools.boollist2sum"
445 (p as Const ("Atools.boollist2sum", _) $
446 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
447 let val isal = isalist2list l
448 val lhss = map lhs isal
449 val sum = list2sum lhss
450 in SOME ((term2str p) ^ " = " ^ (term2str sum),
451 Trueprop $ (mk_equality (p, sum)))
453 | eval_boollist2sum _ _ _ _ = NONE;
462 fun termlessI (_:subst) uv = termless uv;
463 fun term_ordI (_:subst) uv = term_ord uv;
467 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
471 append_rls "list_rls" list_rls
472 [Calc ("op *",eval_binop "#mult_"),
473 Calc ("op +", eval_binop "#add_"),
474 Calc ("op <",eval_equ "#less_"),
475 Calc ("op <=",eval_equ "#less_equal_"),
476 Calc ("Atools.ident",eval_ident "#ident_"),
477 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
479 Calc ("Tools.Vars",eval_var "#Vars_"),
481 Thm ("if_True",num_str if_True),
482 Thm ("if_False",num_str if_False)
485 ruleset' := overwritelthy thy (!ruleset',
486 [("list_rls",list_rls)
489 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
490 val tless_true = dummy_ord;
491 rew_ord' := overwritel (!rew_ord',
492 [("tless_true", tless_true),
493 ("e_rew_ord'", tless_true),
494 ("dummy_ord", dummy_ord)]);
496 val calculate_Atools =
497 append_rls "calculate_Atools" e_rls
498 [Calc ("op <",eval_equ "#less_"),
499 Calc ("op <=",eval_equ "#less_equal_"),
500 Calc ("op =",eval_equal "#equal_"),
502 Thm ("real_unari_minus",num_str real_unari_minus),
503 Calc ("op +",eval_binop "#add_"),
504 Calc ("op -",eval_binop "#sub_"),
505 Calc ("op *",eval_binop "#mult_")
509 append_rls "Atools_erls" e_rls
510 [Calc ("op =",eval_equal "#equal_"),
511 Thm ("not_true",num_str not_true),
512 (*"(~ True) = False"*)
513 Thm ("not_false",num_str not_false),
514 (*"(~ False) = True"*)
515 Thm ("and_true",and_true),
516 (*"(?a & True) = ?a"*)
517 Thm ("and_false",and_false),
518 (*"(?a & False) = False"*)
519 Thm ("or_true",or_true),
520 (*"(?a | True) = True"*)
521 Thm ("or_false",or_false),
522 (*"(?a | False) = ?a"*)
524 Thm ("rat_leq1",rat_leq1),
525 Thm ("rat_leq2",rat_leq2),
526 Thm ("rat_leq3",rat_leq3),
527 Thm ("refl",num_str refl),
528 Thm ("le_refl",num_str le_refl),
529 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
531 Calc ("op <",eval_equ "#less_"),
532 Calc ("op <=",eval_equ "#less_equal_"),
534 Calc ("Atools.ident",eval_ident "#ident_"),
535 Calc ("Atools.is'_const",eval_const "#is_const_"),
536 Calc ("Atools.occurs'_in",eval_occurs_in ""),
537 Calc ("Tools.matches",eval_matches "")
541 append_rls "Atools_crls" e_rls
542 [Calc ("op =",eval_equal "#equal_"),
543 Thm ("not_true",num_str not_true),
544 Thm ("not_false",num_str not_false),
545 Thm ("and_true",and_true),
546 Thm ("and_false",and_false),
547 Thm ("or_true",or_true),
548 Thm ("or_false",or_false),
550 Thm ("rat_leq1",rat_leq1),
551 Thm ("rat_leq2",rat_leq2),
552 Thm ("rat_leq3",rat_leq3),
553 Thm ("refl",num_str refl),
554 Thm ("le_refl",num_str le_refl),
555 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
557 Calc ("op <",eval_equ "#less_"),
558 Calc ("op <=",eval_equ "#less_equal_"),
560 Calc ("Atools.ident",eval_ident "#ident_"),
561 Calc ("Atools.is'_const",eval_const "#is_const_"),
562 Calc ("Atools.occurs'_in",eval_occurs_in ""),
563 Calc ("Tools.matches",eval_matches "")
566 (*val atools_erls = ... waere zu testen ...
567 merge_rls calculate_Atools
568 (append_rls Atools_erls (*i.A. zu viele rules*)
569 [Calc ("Atools.ident",eval_ident "#ident_"),
570 Calc ("Atools.is'_const",eval_const "#is_const_"),
571 Calc ("Atools.occurs'_in",
572 eval_occurs_in "#occurs_in"),
573 Calc ("Tools.matches",eval_matches "#matches")
574 ] (*i.A. zu viele rules*)
576 (* val atools_erls = prep_rls(
577 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
578 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
579 rules = [Thm ("refl",num_str refl),
580 Thm ("le_refl",num_str le_refl),
581 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
582 Thm ("not_true",num_str not_true),
583 Thm ("not_false",num_str not_false),
584 Thm ("and_true",and_true),
585 Thm ("and_false",and_false),
586 Thm ("or_true",or_true),
587 Thm ("or_false",or_false),
588 Thm ("and_commute",num_str and_commute),
589 Thm ("or_commute",num_str or_commute),
591 Calc ("op <",eval_equ "#less_"),
592 Calc ("op <=",eval_equ "#less_equal_"),
594 Calc ("Atools.ident",eval_ident "#ident_"),
595 Calc ("Atools.is'_const",eval_const "#is_const_"),
596 Calc ("Atools.occurs'_in",eval_occurs_in ""),
597 Calc ("Tools.matches",eval_matches "")
599 scr = Script ((term_of o the o (parse thy))
602 ruleset' := overwritelth thy
604 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
607 "******* Atools.ML end *******";
609 calclist':= overwritel (!calclist',
610 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
612 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
613 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
614 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
615 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
616 ("le" ,("op <" ,eval_equ "#less_")),
617 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
618 ("ident" ,("Atools.ident",eval_ident "#ident_")),
619 ("equal" ,("op =",eval_equal "#equal_")),
620 ("PLUS" ,("op +" ,eval_binop "#add_")),
621 ("minus" ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls
622 no script with "minus"*)
623 ("TIMES" ,("op *" ,eval_binop "#mult_")),
624 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
625 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
626 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
629 val list_rls = prep_rls(
630 merge_rls "list_erls"
631 (Rls {id="replaced",preconds = [],
632 rew_ord = ("termlessI", termlessI),
633 erls = Rls {id="list_elrs", preconds = [],
634 rew_ord = ("termlessI",termlessI),
636 srls = Erls, calc = [], (*asm_thm = [],*)
637 rules = [Calc ("op +", eval_binop "#add_"),
638 Calc ("op <",eval_equ "#less_")
639 (* ~~~~~~ for nth_Cons_*)
642 srls = Erls, calc = [], (*asm_thm = [], *)
643 rules = [], scr = EmptyScr})
645 ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]);