1 (* Title: tools for arithmetic
2 Author: Walther Neuper 010308
3 (c) due to copyright terms
6 theory Atools imports Descript Script
9 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
17 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
18 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
20 pow :: "[real, real] => real" (infixr "^^^" 80)
21 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
23 (*WN0603 at FE-interface encoded strings to '^',
24 see 'fun encode', fun 'decode'*)
26 abs :: "real => real" ("(|| _ ||)")
27 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
28 absset :: "real set => real" ("(||| _ |||)")
29 (*is numeral constant ?*)
30 is'_const :: "real => bool" ("_ is'_const" 10)
31 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
32 is'_atom :: "real => bool" ("_ is'_atom" 10)
33 is'_even :: "real => bool" ("_ is'_even" 10)
35 (* identity on term level*)
36 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
38 argument'_in :: "real => real" ("argument'_in _" 10)
39 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
40 WN0609 changed the id, because ".. _ _" inhibits currying**)
41 filter'_sameFunId:: "[real, bool list] => bool list"
42 ("filter'_sameFunId _ _" 10)
43 boollist2sum :: "bool list => real"
44 lastI :: "'a list \<Rightarrow> 'a"
46 axiomatization where (*for evaluating the assumptions of conditional rules*)
48 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
49 real_unari_minus: "- a = (-1) * a" and
51 rle_refl: "(n::real) <= n" and
52 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
53 not_true: "(~ True) = False" and
54 not_false: "(~ False) = True"
56 axiomatization where (*..if replaced by "and" we get error:
57 Type unification failed: No type arity bool :: zero ...*)
58 and_true: "(a & True) = a" and
59 and_false: "(a & False) = False" and
60 or_true: "(a | True) = True" and
61 or_false: "(a | False) = a" and
62 and_commute: "(a & b) = (b & a)" and
63 or_commute: "(a | b) = (b | a)"
65 (*.should be in Rational.thy, but:
66 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
67 axiomatization where (*..if replaced by "and" we get error:
68 Type unification failed: No type arity bool :: zero ...*)
69 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
70 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
72 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
74 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
77 text {*copy from doc/math-eng.tex WN.28.3.03
80 section {*Coding standards*}
81 subsection {*Identifiers*}
82 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).
84 This are the preliminary rules for naming identifiers>
86 \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}.
87 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
88 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
89 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
95 subsection {*Rule sets*}
96 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.
98 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.
101 \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).
103 \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.
105 \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.
106 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).
109 The above rulesets are all visible to the user, and also may be input;
110 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
111 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
112 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
113 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
121 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
127 (** evaluation of numerals and special predicates on the meta-level **)
128 (*-------------------------functions---------------------*)
129 local (* rlang 09.02 *)
130 (*.a 'c is coefficient of v' if v does occur in c.*)
131 fun coeff_in v c = member op = (TermC.vars c) v;
133 fun occurs_in v t = coeff_in v t;
136 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
137 fun eval_occurs_in _ "Atools.occurs'_in"
138 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
139 ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
140 tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
142 then SOME ((Rule.term2str p) ^ " = True",
143 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
144 else SOME ((Rule.term2str p) ^ " = False",
145 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
146 | eval_occurs_in _ _ _ _ = NONE;
148 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
149 fun some_occur_in vs t =
150 let fun occurs_in' a b = occurs_in b a
151 in foldl or_ (false, map (occurs_in' t) vs) end;
153 (*("some_occur_in", ("Atools.some'_occur'_in",
154 eval_some_occur_in "#eval_some_occur_in_"))*)
155 fun eval_some_occur_in _ "Atools.some'_occur'_in"
156 (p as (Const ("Atools.some'_occur'_in",_)
158 if some_occur_in (TermC.isalist2list vs) t
159 then SOME ((Rule.term2str p) ^ " = True",
160 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
161 else SOME ((Rule.term2str p) ^ " = False",
162 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
163 | eval_some_occur_in _ _ _ _ = NONE;
168 (*evaluate 'is_atom'*)
169 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
170 fun eval_is_atom (thmid:string) "Atools.is'_atom"
171 (t as (Const(op0,_) $ arg)) thy =
173 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
174 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
175 | _ => SOME (TermC.mk_thmid thmid "" "",
176 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
177 | eval_is_atom _ _ _ _ = NONE;
179 (*evaluate 'is_even'*)
180 fun even i = (i div 2) * 2 = i;
181 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
182 fun eval_is_even (thmid:string) "Atools.is'_even"
183 (t as (Const(op0,_) $ arg)) thy =
186 (case TermC.int_of_str_opt n of
188 if even i then SOME (TermC.mk_thmid thmid n "",
189 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
190 else SOME (TermC.mk_thmid thmid "" "",
191 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
194 | eval_is_even _ _ _ _ = NONE;
196 (*evaluate 'is_const'*)
197 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
198 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
199 (t as (Const(op0,t0) $ arg)) (thy:theory) =
200 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
203 SOME (TermC.mk_thmid thmid n1 "",
204 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
207 then SOME (TermC.mk_thmid thmid n1 "",
208 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
209 else SOME (TermC.mk_thmid thmid n1 "",
210 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
211 | Const ("Float.Float",_) =>
212 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
213 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
215 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
216 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
217 | eval_const _ _ _ _ = NONE;
219 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
220 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
221 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
222 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
224 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
225 ("xxxxxx",op_,t,thy);
227 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
229 (string_of_int v11)^","^(string_of_int v12)^"), ("^
230 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
231 (string_of_int v21)^","^(string_of_int v22)^"), ("^
232 (string_of_int p21)^","^(string_of_int p22)^"))";
234 (*.convert int and float to internal floatingpoint prepresentation.*)
235 fun numeral (Free (str, T)) =
236 (case TermC.int_of_str_opt str of
237 SOME i => SOME ((i, 0), (0, 0))
239 | numeral (Const ("Float.Float", _) $
240 (Const ("Product_Type.Pair", _) $
241 (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
242 (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
243 (case (TermC.int_of_str_opt v1, TermC.int_of_str_opt v2, TermC.int_of_str_opt p1, TermC.int_of_str_opt p2) of
244 (SOME v1', SOME v2', SOME p1', SOME p2') =>
245 SOME ((v1', v2'), (p1', p2'))
249 (* evaluate binary associative operations *)
250 fun eval_binop (thmid : string) (op_: string)
251 (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
253 case (numeral t1, numeral t2) of
254 (SOME n1, SOME n2) =>
256 val (T1, _, _) = TermC.dest_binop_typ t0
258 calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
259 (*WN071229 "Rings.divide_class.divide" never tried*)
260 val rhs = var_op_float v op_ t0 T1 res
261 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
262 in SOME ("#: " ^ Rule.term2str prop, prop) end
265 | eval_binop (thmid : string) (op_ : string)
266 (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
268 case (numeral t1, numeral t2) of
269 (SOME n1, SOME n2) =>
270 if op0 = "Groups.minus_class.minus" then NONE
272 val (T1, _, _) = TermC.dest_binop_typ t0
273 val res = calcul op0 n1 n2
274 val rhs = float_op_var v op_ t0 T1 res
275 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
276 in SOME ("#: " ^ Rule.term2str prop, prop) end
279 | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
280 (case (numeral t1, numeral t2) of
281 (SOME n1, SOME n2) =>
283 val (_, _, Trange) = TermC.dest_binop_typ t0;
284 val res = calcul op0 n1 n2;
285 val rhs = term_of_float Trange res;
286 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
287 in SOME ("#: " ^ Rule.term2str prop, prop) end
289 | eval_binop _ _ _ _ = NONE;
291 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
293 val it = "-1 + 2 = 1"
294 > val t = str2term "-1 * (-1 * a)";
295 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
297 val it = "-1 * (-1 * a) = 1 * a"*)
301 (*.evaluate < and <= for numerals.*)
302 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
303 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
304 fun eval_equ (thmid:string) (op_:string) (t as
305 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
306 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
307 (SOME n1', SOME n2') =>
308 if Calc.calc_equ (strip_thy op0) (n1', n2')
309 then SOME (TermC.mk_thmid thmid n1 n2,
310 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
311 else SOME (TermC.mk_thmid thmid n1 n2,
312 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
315 | eval_equ _ _ _ _ = NONE;
320 val it = "(?t = ?t) = True"
321 > val t = str2term "x = 0";
322 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
324 > val t = str2term "1 = 0";
325 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
326 ----------- thus needs Rule.Calc !
327 > val t = str2term "0 = 0";
328 > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
332 val t = str2term "Not (x = 0)";
333 atomt t; Rule.term2str t;
339 val it = "x ~= 0" : string*)
341 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
342 the arguments: thus special handling by 'fun eval_binop'*)
343 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
344 fun eval_ident (thmid:string) "Atools.ident" (t as
345 (Const (op0,t0) $ t1 $ t2 )) thy =
347 then SOME (TermC.mk_thmid thmid
348 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
349 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
350 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
351 else SOME (TermC.mk_thmid thmid
352 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
353 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
354 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
355 | eval_ident _ _ _ _ = NONE;
357 > val t = str2term "x =!= 0";
358 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
360 val str = "ident_(x)_(0)" : string
361 val it = "(x =!= 0) = False" : string
362 > val t = str2term "1 =!= 0";
363 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
365 val str = "ident_(1)_(0)" : string
366 val it = "(1 =!= 0) = False" : string
367 > val t = str2term "0 =!= 0";
368 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
370 val str = "ident_(0)_(0)" : string
371 val it = "(0 =!= 0) = True" : string
374 (*.evaluate identity of terms, which stay ready for evaluation in turn;
375 thus returns False only for atoms.*)
376 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
377 fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy =
379 then SOME (TermC.mk_thmid thmid
380 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
381 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
382 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
383 else (case (TermC.is_atom t1, TermC.is_atom t2) of
385 SOME (TermC.mk_thmid thmid
386 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
387 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
388 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
389 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
390 | eval_equal _ _ _ _ = NONE; (* error-exit *)
392 val t = str2term "x ~= 0";
393 val NONE = eval_equal "equal_" "b" t thy;
396 > val t = str2term "(x + 1) = (x + 1)";
397 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
399 val str = "equal_(x + 1)_(x + 1)" : string
400 val it = "(x + 1 = x + 1) = True" : string
401 > val t = str2term "x = 0";
402 > val NONE = eval_equal "equal_" "b" t thy;
404 > val t = str2term "1 = 0";
405 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
407 val str = "equal_(1)_(0)" : string
408 val it = "(1 = 0) = False" : string
409 > val t = str2term "0 = 0";
410 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
412 val str = "equal_(0)_(0)" : string
413 val it = "(0 = 0) = True" : string
420 (** evaluation on the metalevel **)
422 (*. evaluate HOL.divide .*)
423 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
424 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
425 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
426 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
427 (SOME n1', SOME n2') =>
429 val sg = Calc.sign_mult n1' n2';
430 val (T1,T2,Trange) = TermC.dest_binop_typ t0;
431 val gcd' = Calc.gcd (abs n1') (abs n2');
433 then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
434 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
435 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
436 else if 0 < n2' andalso gcd' = 1 then NONE
437 else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
439 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
440 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
442 | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
444 | eval_cancel _ _ _ _ = NONE;
446 (*. get the argument from a function-definition.*)
447 (*("argument_in" ,("Atools.argument'_in",
448 eval_argument_in "Atools.argument'_in"))*)
449 fun eval_argument_in _ "Atools.argument'_in"
450 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
451 if is_Free arg (*could be something to be simplified before*)
452 then SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
453 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
455 | eval_argument_in _ _ _ _ = NONE;
457 (*.check if the function-identifier of the first argument matches
458 the function-identifier of the lhs of the second argument.*)
459 (*("sameFunId" ,("Atools.sameFunId",
460 eval_same_funid "Atools.sameFunId"))*)
461 fun eval_sameFunId _ "Atools.sameFunId"
462 (p as Const ("Atools.sameFunId",_) $
464 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
466 then SOME ((Rule.term2str p) ^ " = True",
467 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
468 else SOME ((Rule.term2str p) ^ " = False",
469 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
470 | eval_sameFunId _ _ _ _ = NONE;
473 (*.from a list of fun-definitions "f x = ..." as 2nd argument
474 filter the elements with the same fun-identfier in "f y"
476 this is, because Isabelles filter takes more than 1 sec.*)
477 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
478 | same_funid f1 t = error ("same_funid called with t = ("
479 ^Rule.term2str f1^") ("^Rule.term2str t^")");
480 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
481 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
482 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
483 (p as Const ("Atools.filter'_sameFunId",_) $
485 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
486 (filter (same_funid fid))) (TermC.isalist2list fs)
487 in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
488 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
489 | eval_filter_sameFunId _ _ _ _ = NONE;
492 (*make a list of terms to a sum*)
493 fun list2sum [] = error ("list2sum called with []")
496 let fun sum su [s'] =
497 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
500 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
504 (*make a list of equalities to the sum of the lhs*)
505 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
506 fun eval_boollist2sum _ "Atools.boollist2sum"
507 (p as Const ("Atools.boollist2sum", _) $
508 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
509 let val isal = TermC.isalist2list l
510 val lhss = map lhs isal
511 val sum = list2sum lhss
512 in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
513 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
515 | eval_boollist2sum _ _ _ _ = NONE;
524 fun termlessI (_: Rule.subst) uv = Term_Ord.termless uv;
525 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
529 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
532 val list_rls = Rule.append_rls "list_rls" list_rls
533 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
534 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
535 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
536 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
537 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
538 Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
540 Rule.Calc ("Tools.Vars",eval_var "#Vars_"),
542 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
543 Rule.Thm ("if_False",TermC.num_str @{thm if_False})
548 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
549 val tless_true = Rule.dummy_ord;
550 Rule.rew_ord' := overwritel (! Rule.rew_ord',
551 [("tless_true", tless_true),
552 ("e_rew_ord'", tless_true),
553 ("dummy_ord", Rule.dummy_ord)]);
555 val calculate_Base_Tools =
556 Rule.append_rls "calculate_Atools" Rule.e_rls
557 [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
558 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
559 Rule.Calc ("HOL.eq",eval_equal "#equal_"),
561 Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
562 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
563 Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
564 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_")
569 find_theorems (9) "?n <= ?n"
573 Rule.append_rls "Atools_erls" Rule.e_rls
574 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
575 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
576 (*"(~ True) = False"*)
577 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
578 (*"(~ False) = True"*)
579 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
580 (*"(?a & True) = ?a"*)
581 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
582 (*"(?a & False) = False"*)
583 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
584 (*"(?a | True) = True"*)
585 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
586 (*"(?a | False) = ?a"*)
588 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
589 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
590 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
591 Rule.Thm ("refl",TermC.num_str @{thm refl}),
592 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
593 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
595 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
596 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
598 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
599 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
600 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
601 Rule.Calc ("Tools.matches",eval_matches "")
608 Rule.append_rls "Atools_crls" Rule.e_rls
609 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
610 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
611 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
612 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
613 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
614 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
615 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
617 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
618 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
619 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
620 Rule.Thm ("refl",TermC.num_str @{thm refl}),
621 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
622 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
624 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
625 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
627 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
628 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
629 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
630 Rule.Calc ("Tools.matches",eval_matches "")
633 (*val atools_erls = ... waere zu testen ...
634 Rule.merge_rls calculate_Atools
635 (Rule.append_rls Atools_erls (*i.A. zu viele rules*)
636 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
637 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
638 Rule.Calc ("Atools.occurs'_in",
639 eval_occurs_in "#occurs_in"),
640 Rule.Calc ("Tools.matches",eval_matches "#matches")
641 ] (*i.A. zu viele rules*)
643 (* val atools_erls = prep_rls'( (*outcommented*)
644 Rule.Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
645 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
646 rules = [Rule.Thm ("refl",num_str @{thm refl}),
647 Rule.Thm ("order_refl",num_str @{thm order_refl}),
648 Rule.Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
649 Rule.Thm ("not_true",num_str @{thm not_true}),
650 Rule.Thm ("not_false",num_str @{thm not_false}),
651 Rule.Thm ("and_true",num_str @{thm and_true}),
652 Rule.Thm ("and_false",num_str @{thm and_false}),
653 Rule.Thm ("or_true",num_str @{thm or_true}),
654 Rule.Thm ("or_false",num_str @{thm or_false}),
655 Rule.Thm ("and_commute",num_str @{thm and_commute}),
656 Rule.Thm ("or_commute",num_str @{thm or_commute}),
658 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
659 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
661 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
662 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
663 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
664 Rule.Calc ("Tools.matches",eval_matches "")
666 scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
669 "******* Atools.ML end *******";
671 setup {* KEStore_Elems.add_calcs
672 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
674 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
675 ("is_atom" ,("Atools.is'_atom", eval_is_atom "#is_atom_")),
676 ("is_even" ,("Atools.is'_even", eval_is_even "#is_even_")),
677 ("is_const" ,("Atools.is'_const", eval_const "#is_const_")),
678 ("le" ,("Orderings.ord_class.less", eval_equ "#less_")),
679 ("leq" ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
680 ("ident" ,("Atools.ident", eval_ident "#ident_")),
681 ("equal" ,("HOL.eq", eval_equal "#equal_")),
682 ("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
683 ("MINUS" ,("Groups.minus_class.minus", eval_binop "#sub_")),
684 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
685 ("DIVIDE" ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
686 ("POWER" ,("Atools.pow", eval_binop "#power_")),
687 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
689 val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
690 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
691 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
692 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
693 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
694 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
695 (* ~~~~~~ for nth_Cons_*)],
696 scr = Rule.EmptyScr},
697 srls = Rule.Erls, calc = [], errpatts = [],
698 rules = [], scr = Rule.EmptyScr})
701 setup {* KEStore_Elems.add_rlss
702 [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))] *}