1 (* Title: tools for arithmetic
2 Author: Walther Neuper 010308
3 (c) due to copyright terms
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
9 theory Atools imports Descript "../Interpret/Interpret" "../xmlsrc/xmlsrc"
18 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
19 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
21 pow :: "[real, real] => real" (infixr "^^^" 80)
22 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
24 (*WN0603 at FE-interface encoded strings to '^',
25 see 'fun encode', fun 'decode'*)
27 abs :: "real => real" ("(|| _ ||)")
28 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
29 absset :: "real set => real" ("(||| _ |||)")
30 (*is numeral constant ?*)
31 is'_const :: "real => bool" ("_ is'_const" 10)
32 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
33 is'_atom :: "real => bool" ("_ is'_atom" 10)
34 is'_even :: "real => bool" ("_ is'_even" 10)
36 (* identity on term level*)
37 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
39 argument'_in :: "real => real" ("argument'_in _" 10)
40 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
41 WN0609 changed the id, because ".. _ _" inhibits currying**)
42 filter'_sameFunId:: "[real, bool list] => bool list"
43 ("filter'_sameFunId _ _" 10)
44 boollist2sum :: "bool list => real"
46 axioms (*for evaluating the assumptions of conditional rules*)
48 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
49 real_unari_minus: "- a = (-1) * a"
51 rle_refl: "(n::real) <= n"
52 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
53 not_true: "(~ True) = False"
54 not_false: "(~ False) = True"
55 and_true: "(a & True) = a"
56 and_false: "(a & False) = False"
57 or_true: "(a | True) = True"
58 or_false: "(a | False) = a"
59 and_commute: "(a & b) = (b & a)"
60 or_commute: "(a | b) = (b | a)"
62 (*.should be in Rational.thy, but:
63 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
64 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
65 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
67 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
69 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
72 text {*copy from doc/math-eng.tex WN.28.3.03
75 section {*Coding standards*}
76 subsection {*Identifiers*}
77 text {*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).
79 This are the preliminary rules for naming identifiers>
81 \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}.
82 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
83 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
84 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
90 subsection {*Rule sets*}
91 text {*The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
93 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.
96 \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).
98 \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.
100 \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.
101 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).
104 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.
105 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
113 {\tt append_rls, merge_rls, remove_rls} TODO
119 (** evaluation of numerals and special predicates on the meta-level **)
120 (*-------------------------functions---------------------*)
121 local (* rlang 09.02 *)
122 (*.a 'c is coefficient of v' if v does occur in c.*)
123 fun coeff_in v c = member op = (vars c) v;
125 fun occurs_in v t = coeff_in v t;
128 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
129 fun eval_occurs_in _ "Atools.occurs'_in"
130 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
131 ((*tracing("@@@ eval_occurs_in: v= "^(term2str v));
132 tracing("@@@ eval_occurs_in: t= "^(term2str t));*)
134 then SOME ((term2str p) ^ " = True",
135 Trueprop $ (mk_equality (p, HOLogic.true_const)))
136 else SOME ((term2str p) ^ " = False",
137 Trueprop $ (mk_equality (p, HOLogic.false_const))))
138 | eval_occurs_in _ _ _ _ = NONE;
140 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
141 fun some_occur_in vs t =
142 let fun occurs_in' a b = occurs_in b a
143 in foldl or_ (false, map (occurs_in' t) vs) end;
145 (*("some_occur_in", ("Atools.some'_occur'_in",
146 eval_some_occur_in "#eval_some_occur_in_"))*)
147 fun eval_some_occur_in _ "Atools.some'_occur'_in"
148 (p as (Const ("Atools.some'_occur'_in",_)
150 if some_occur_in (isalist2list vs) t
151 then SOME ((term2str p) ^ " = True",
152 Trueprop $ (mk_equality (p, HOLogic.true_const)))
153 else SOME ((term2str p) ^ " = False",
154 Trueprop $ (mk_equality (p, HOLogic.false_const)))
155 | eval_some_occur_in _ _ _ _ = NONE;
160 (*evaluate 'is_atom'*)
161 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
162 fun eval_is_atom (thmid:string) "Atools.is'_atom"
163 (t as (Const(op0,_) $ arg)) thy =
165 Free (n,_) => SOME (mk_thmid thmid op0 n "",
166 Trueprop $ (mk_equality (t, true_as_term)))
167 | _ => SOME (mk_thmid thmid op0 "" "",
168 Trueprop $ (mk_equality (t, false_as_term))))
169 | eval_is_atom _ _ _ _ = NONE;
171 (*evaluate 'is_even'*)
172 fun even i = (i div 2) * 2 = i;
173 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
174 fun eval_is_even (thmid:string) "Atools.is'_even"
175 (t as (Const(op0,_) $ arg)) thy =
178 (case int_of_str n of
180 if even i then SOME (mk_thmid thmid op0 n "",
181 Trueprop $ (mk_equality (t, true_as_term)))
182 else SOME (mk_thmid thmid op0 "" "",
183 Trueprop $ (mk_equality (t, false_as_term)))
186 | eval_is_even _ _ _ _ = NONE;
188 (*evaluate 'is_const'*)
189 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
190 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
191 (t as (Const(op0,t0) $ arg)) (thy:theory) =
192 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
195 SOME (mk_thmid thmid op0 n1 "",
196 Trueprop $ (mk_equality (t, false_as_term)))
199 then SOME (mk_thmid thmid op0 n1 "",
200 Trueprop $ (mk_equality (t, true_as_term)))
201 else SOME (mk_thmid thmid op0 n1 "",
202 Trueprop $ (mk_equality (t, false_as_term)))
203 | Const ("Float.Float",_) =>
204 SOME (mk_thmid thmid op0 (term2str arg) "",
205 Trueprop $ (mk_equality (t, true_as_term)))
207 SOME (mk_thmid thmid op0 (term2str arg) "",
208 Trueprop $ (mk_equality (t, false_as_term))))
209 | eval_const _ _ _ _ = NONE;
211 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
212 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
213 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
214 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
216 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
217 ("xxxxxx",op_,t,thy);
219 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
221 (string_of_int v11)^","^(string_of_int v12)^"), ("^
222 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
223 (string_of_int v21)^","^(string_of_int v22)^"), ("^
224 (string_of_int p21)^","^(string_of_int p22)^"))";
226 (*.convert int and float to internal floatingpoint prepresentation.*)
227 fun numeral (Free (str, T)) =
228 (case int_of_str str of
229 SOME i => SOME ((i, 0), (0, 0))
231 | numeral (Const ("Float.Float", _) $
233 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
234 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
235 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
236 (SOME v1', SOME v2', SOME p1', SOME p2') =>
237 SOME ((v1', v2'), (p1', p2'))
241 (*.evaluate binary associative operations.*)
242 fun eval_binop (thmid:string) (op_:string)
243 (t as ( Const(op0,t0) $
244 (Const(op0',t0') $ v $ t1) $ t2))
245 thy = (*binary . (v.n1).n2*)
247 case (numeral t1, numeral t2) of
248 (SOME n1, SOME n2) =>
249 let val (T1,T2,Trange) = dest_binop_typ t0
250 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
251 (*WN071229 "Rings.inverse_class.divide" never tried*)
252 val rhs = var_op_float v op_ t0 T1 res
253 val prop = Trueprop $ (mk_equality (t, rhs))
254 in SOME (mk_thmid_f thmid n1 n2, prop) end
257 | eval_binop (thmid:string) (op_:string)
259 (Const (op0, t0) $ t1 $
260 (Const (op0', t0') $ t2 $ v)))
261 thy = (*binary . n1.(n2.v)*)
263 case (numeral t1, numeral t2) of
264 (SOME n1, SOME n2) =>
265 if op0 = "Groups.minus_class.minus" then NONE else
266 let val (T1,T2,Trange) = dest_binop_typ t0
267 val res = calc op0 n1 n2
268 val rhs = float_op_var v op_ t0 T1 res
269 val prop = Trueprop $ (mk_equality (t, rhs))
270 in SOME (mk_thmid_f thmid n1 n2, prop) end
274 | eval_binop (thmid:string) (op_:string)
275 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
276 (case (numeral t1, numeral t2) of
277 (SOME n1, SOME n2) =>
278 let val (T1,T2,Trange) = dest_binop_typ t0;
279 val res = calc op0 n1 n2;
280 val rhs = term_of_float Trange res;
281 val prop = Trueprop $ (mk_equality (t, rhs));
282 in SOME (mk_thmid_f thmid n1 n2, prop) end
284 | eval_binop _ _ _ _ = NONE;
286 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
288 val it = "-1 + 2 = 1"
289 > val t = str2term "-1 * (-1 * a)";
290 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
292 val it = "-1 * (-1 * a) = 1 * a"*)
296 (*.evaluate < and <= for numerals.*)
297 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
298 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
299 fun eval_equ (thmid:string) (op_:string) (t as
300 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
301 (case (int_of_str n1, int_of_str n2) of
302 (SOME n1', SOME n2') =>
303 if calc_equ (strip_thy op0) (n1', n2')
304 then SOME (mk_thmid thmid op0 n1 n2,
305 Trueprop $ (mk_equality (t, true_as_term)))
306 else SOME (mk_thmid thmid op0 n1 n2,
307 Trueprop $ (mk_equality (t, false_as_term)))
310 | eval_equ _ _ _ _ = NONE;
315 val it = "(?t = ?t) = True"
316 > val t = str2term "x = 0";
317 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
319 > val t = str2term "1 = 0";
320 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
321 ----------- thus needs Calc !
322 > val t = str2term "0 = 0";
323 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
327 val t = str2term "Not (x = 0)";
334 val it = "x ~= 0" : string*)
336 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
337 the arguments: thus special handling by 'fun eval_binop'*)
338 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
339 fun eval_ident (thmid:string) "Atools.ident" (t as
340 (Const (op0,t0) $ t1 $ t2 )) thy =
342 then SOME (mk_thmid thmid op0
343 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
344 (thy2ctxt thy)) t1) ^ ")")
345 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
346 (thy2ctxt thy)) t2) ^ ")"),
347 Trueprop $ (mk_equality (t, true_as_term)))
348 else SOME (mk_thmid thmid op0
349 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
350 (thy2ctxt thy)) t1) ^ ")")
351 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
352 (thy2ctxt thy)) t2) ^ ")"),
353 Trueprop $ (mk_equality (t, false_as_term)))
354 | eval_ident _ _ _ _ = NONE;
356 > val t = str2term "x =!= 0";
357 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
359 val str = "ident_(x)_(0)" : string
360 val it = "(x =!= 0) = False" : string
361 > val t = str2term "1 =!= 0";
362 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
364 val str = "ident_(1)_(0)" : string
365 val it = "(1 =!= 0) = False" : string
366 > val t = str2term "0 =!= 0";
367 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
369 val str = "ident_(0)_(0)" : string
370 val it = "(0 =!= 0) = True" : string
373 (*.evaluate identity of terms, which stay ready for evaluation in turn;
374 thus returns False only for atoms.*)
375 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
376 fun eval_equal (thmid : string) "HOL.eq" (t as
377 (Const (op0,t0) $ t1 $ t2 )) thy =
379 then SOME (mk_thmid thmid op0
380 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
383 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
386 Trueprop $ (mk_equality (t, true_as_term)))
387 else (case (is_atom t1, is_atom t2) of
389 SOME (mk_thmid thmid op0
390 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
393 Print_Mode.setmp [] (Syntax.string_of_term
396 Trueprop $ (mk_equality (t, false_as_term)))
397 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
398 | eval_equal _ _ _ _ = NONE; (* error-exit *)
400 val t = str2term "x ~= 0";
401 val NONE = eval_equal "equal_" "b" t thy;
404 > val t = str2term "(x + 1) = (x + 1)";
405 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
407 val str = "equal_(x + 1)_(x + 1)" : string
408 val it = "(x + 1 = x + 1) = True" : string
409 > val t = str2term "x = 0";
410 > val NONE = eval_equal "equal_" "b" t thy;
412 > val t = str2term "1 = 0";
413 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
415 val str = "equal_(1)_(0)" : string
416 val it = "(1 = 0) = False" : string
417 > val t = str2term "0 = 0";
418 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
420 val str = "equal_(0)_(0)" : string
421 val it = "(0 = 0) = True" : string
425 (** evaluation on the metalevel **)
427 (*. evaluate HOL.divide .*)
428 (*("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e"))*)
429 fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as
430 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
431 (case (int_of_str n1, int_of_str n2) of
432 (SOME n1', SOME n2') =>
434 val sg = sign2 n1' n2';
435 val (T1,T2,Trange) = dest_binop_typ t0;
436 val gcd' = gcd (abs n1') (abs n2');
438 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
439 val prop = Trueprop $ (mk_equality (t, rhs))
440 in SOME (mk_thmid thmid op0 n1 n2, prop) end
441 else if 0 < n2' andalso gcd' = 1 then NONE
442 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
444 val prop = Trueprop $ (mk_equality (t, rhs))
445 in SOME (mk_thmid thmid op0 n1 n2, prop) end
447 | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
449 | eval_cancel _ _ _ _ = NONE;
451 (*. get the argument from a function-definition.*)
452 (*("argument_in" ,("Atools.argument'_in",
453 eval_argument_in "Atools.argument'_in"))*)
454 fun eval_argument_in _ "Atools.argument'_in"
455 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
456 if is_Free arg (*could be something to be simplified before*)
457 then SOME (term2str t ^ " = " ^ term2str arg,
458 Trueprop $ (mk_equality (t, arg)))
460 | eval_argument_in _ _ _ _ = NONE;
462 (*.check if the function-identifier of the first argument matches
463 the function-identifier of the lhs of the second argument.*)
464 (*("sameFunId" ,("Atools.sameFunId",
465 eval_same_funid "Atools.sameFunId"))*)
466 fun eval_sameFunId _ "Atools.sameFunId"
467 (p as Const ("Atools.sameFunId",_) $
469 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
471 then SOME ((term2str p) ^ " = True",
472 Trueprop $ (mk_equality (p, HOLogic.true_const)))
473 else SOME ((term2str p) ^ " = False",
474 Trueprop $ (mk_equality (p, HOLogic.false_const)))
475 | eval_sameFunId _ _ _ _ = NONE;
478 (*.from a list of fun-definitions "f x = ..." as 2nd argument
479 filter the elements with the same fun-identfier in "f y"
481 this is, because Isabelles filter takes more than 1 sec.*)
482 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
483 | same_funid f1 t = error ("same_funid called with t = ("
484 ^term2str f1^") ("^term2str t^")");
485 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
486 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
487 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
488 (p as Const ("Atools.filter'_sameFunId",_) $
490 let val fs' = ((list2isalist HOLogic.boolT) o
491 (filter (same_funid fid))) (isalist2list fs)
492 in SOME (term2str (mk_equality (p, fs')),
493 Trueprop $ (mk_equality (p, fs'))) end
494 | eval_filter_sameFunId _ _ _ _ = NONE;
497 (*make a list of terms to a sum*)
498 fun list2sum [] = error ("list2sum called with []")
501 let fun sum su [s'] =
502 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
505 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
509 (*make a list of equalities to the sum of the lhs*)
510 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
511 fun eval_boollist2sum _ "Atools.boollist2sum"
512 (p as Const ("Atools.boollist2sum", _) $
513 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
514 let val isal = isalist2list l
515 val lhss = map lhs isal
516 val sum = list2sum lhss
517 in SOME ((term2str p) ^ " = " ^ (term2str sum),
518 Trueprop $ (mk_equality (p, sum)))
520 | eval_boollist2sum _ _ _ _ = NONE;
529 fun termlessI (_:subst) uv = Term_Ord.termless uv;
530 fun term_ordI (_:subst) uv = Term_Ord.term_ord uv;
534 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
538 append_rls "list_rls" list_rls
539 [Calc ("Groups.times_class.times",eval_binop "#mult_"),
540 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
541 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
542 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
543 Calc ("Atools.ident",eval_ident "#ident_"),
544 Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
546 Calc ("Tools.Vars",eval_var "#Vars_"),
548 Thm ("if_True",num_str @{thm if_True}),
549 Thm ("if_False",num_str @{thm if_False})
552 ruleset' := overwritelthy thy (!ruleset',
553 [("list_rls",list_rls)
556 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
557 val tless_true = dummy_ord;
558 rew_ord' := overwritel (!rew_ord',
559 [("tless_true", tless_true),
560 ("e_rew_ord'", tless_true),
561 ("dummy_ord", dummy_ord)]);
563 val calculate_Atools =
564 append_rls "calculate_Atools" e_rls
565 [Calc ("Orderings.ord_class.less",eval_equ "#less_"),
566 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
567 Calc ("HOL.eq",eval_equal "#equal_"),
569 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
570 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
571 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
572 Calc ("Groups.times_class.times",eval_binop "#mult_")
576 append_rls "Atools_erls" e_rls
577 [Calc ("HOL.eq",eval_equal "#equal_"),
578 Thm ("not_true",num_str @{thm not_true}),
579 (*"(~ True) = False"*)
580 Thm ("not_false",num_str @{thm not_false}),
581 (*"(~ False) = True"*)
582 Thm ("and_true",num_str @{thm and_true}),
583 (*"(?a & True) = ?a"*)
584 Thm ("and_false",num_str @{thm and_false}),
585 (*"(?a & False) = False"*)
586 Thm ("or_true",num_str @{thm or_true}),
587 (*"(?a | True) = True"*)
588 Thm ("or_false",num_str @{thm or_false}),
589 (*"(?a | False) = ?a"*)
591 Thm ("rat_leq1",num_str @{thm rat_leq1}),
592 Thm ("rat_leq2",num_str @{thm rat_leq2}),
593 Thm ("rat_leq3",num_str @{thm rat_leq3}),
594 Thm ("refl",num_str @{thm refl}),
595 Thm ("real_le_refl",num_str @{thm real_le_refl}),
596 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
598 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
599 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
601 Calc ("Atools.ident",eval_ident "#ident_"),
602 Calc ("Atools.is'_const",eval_const "#is_const_"),
603 Calc ("Atools.occurs'_in",eval_occurs_in ""),
604 Calc ("Tools.matches",eval_matches "")
608 append_rls "Atools_crls" e_rls
609 [Calc ("HOL.eq",eval_equal "#equal_"),
610 Thm ("not_true",num_str @{thm not_true}),
611 Thm ("not_false",num_str @{thm not_false}),
612 Thm ("and_true",num_str @{thm and_true}),
613 Thm ("and_false",num_str @{thm and_false}),
614 Thm ("or_true",num_str @{thm or_true}),
615 Thm ("or_false",num_str @{thm or_false}),
617 Thm ("rat_leq1",num_str @{thm rat_leq1}),
618 Thm ("rat_leq2",num_str @{thm rat_leq2}),
619 Thm ("rat_leq3",num_str @{thm rat_leq3}),
620 Thm ("refl",num_str @{thm refl}),
621 Thm ("real_le_refl",num_str @{thm real_le_refl}),
622 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
624 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
625 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
627 Calc ("Atools.ident",eval_ident "#ident_"),
628 Calc ("Atools.is'_const",eval_const "#is_const_"),
629 Calc ("Atools.occurs'_in",eval_occurs_in ""),
630 Calc ("Tools.matches",eval_matches "")
633 (*val atools_erls = ... waere zu testen ...
634 merge_rls calculate_Atools
635 (append_rls Atools_erls (*i.A. zu viele rules*)
636 [Calc ("Atools.ident",eval_ident "#ident_"),
637 Calc ("Atools.is'_const",eval_const "#is_const_"),
638 Calc ("Atools.occurs'_in",
639 eval_occurs_in "#occurs_in"),
640 Calc ("Tools.matches",eval_matches "#matches")
641 ] (*i.A. zu viele rules*)
643 (* val atools_erls = prep_rls(
644 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
645 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
646 rules = [Thm ("refl",num_str @{thm refl}),
647 Thm ("real_le_refl",num_str @{thm real_le_refl}),
648 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
649 Thm ("not_true",num_str @{thm not_true}),
650 Thm ("not_false",num_str @{thm not_false}),
651 Thm ("and_true",num_str @{thm and_true}),
652 Thm ("and_false",num_str @{thm and_false}),
653 Thm ("or_true",num_str @{thm or_true}),
654 Thm ("or_false",num_str @{thm or_false}),
655 Thm ("and_commute",num_str @{thm and_commute}),
656 Thm ("or_commute",num_str @{thm or_commute}),
658 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
659 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
661 Calc ("Atools.ident",eval_ident "#ident_"),
662 Calc ("Atools.is'_const",eval_const "#is_const_"),
663 Calc ("Atools.occurs'_in",eval_occurs_in ""),
664 Calc ("Tools.matches",eval_matches "")
666 scr = Script ((term_of o the o (parse @{theory}))
669 ruleset' := overwritelth @{theory}
671 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
674 "******* Atools.ML end *******";
676 calclist':= overwritel (!calclist',
677 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
679 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
680 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
681 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
682 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
683 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
684 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
685 ("ident" ,("Atools.ident",eval_ident "#ident_")),
686 ("equal" ,("HOL.eq",eval_equal "#equal_")),
687 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
688 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
689 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
690 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
691 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
692 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
695 val list_rls = prep_rls(
696 merge_rls "list_erls"
697 (Rls {id="replaced",preconds = [],
698 rew_ord = ("termlessI", termlessI),
699 erls = Rls {id="list_elrs", preconds = [],
700 rew_ord = ("termlessI",termlessI),
702 srls = Erls, calc = [], (*asm_thm = [],*)
703 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
704 Calc ("Orderings.ord_class.less",eval_equ "#less_")
705 (* ~~~~~~ for nth_Cons_*)
708 srls = Erls, calc = [], (*asm_thm = [], *)
709 rules = [], scr = EmptyScr})
711 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);