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
10 uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")
11 ("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
12 ("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
13 ("Interpret/inform.sml")("Interpret/mathengine.sml")
14 ("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")
15 ("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")
17 use "Interpret/mstools.sml"
18 use "Interpret/ctree.sml"
19 use "Interpret/ptyps.sml" (*^^^ need files for: fun prep_pbt, fun store_pbt*)
20 use "Interpret/generate.sml"
21 use "Interpret/calchead.sml"
22 use "Interpret/appl.sml"
23 use "Interpret/rewtools.sml"
24 use "Interpret/script.sml"
25 use "Interpret/solve.sml"
26 use "Interpret/inform.sml" (*^^^ need files for: fun castab*)
27 use "Interpret/mathengine.sml"
29 use "xmlsrc/mathml.sml"
30 use "xmlsrc/datatypes.sml"
31 use "xmlsrc/pbl-met-hierarchy.sml"
32 use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
33 use "xmlsrc/interface-xml.sml"
41 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
42 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
44 pow :: "[real, real] => real" (infixr "^^^" 80)
45 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
47 (*WN0603 at FE-interface encoded strings to '^',
48 see 'fun encode', fun 'decode'*)
50 abs :: "real => real" ("(|| _ ||)")
51 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
52 absset :: "real set => real" ("(||| _ |||)")
53 (*is numeral constant ?*)
54 is'_const :: "real => bool" ("_ is'_const" 10)
55 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
56 is'_atom :: "real => bool" ("_ is'_atom" 10)
57 is'_even :: "real => bool" ("_ is'_even" 10)
59 (* identity on term level*)
60 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
62 argument'_in :: "real => real" ("argument'_in _" 10)
63 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
64 WN0609 changed the id, because ".. _ _" inhibits currying**)
65 filter'_sameFunId:: "[real, bool list] => bool list"
66 ("filter'_sameFunId _ _" 10)
67 boollist2sum :: "bool list => real"
69 axioms (*for evaluating the assumptions of conditional rules*)
71 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
72 real_unari_minus: "- a = (-1) * a"
74 rle_refl: "(n::real) <= n"
75 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
76 not_true: "(~ True) = False"
77 not_false: "(~ False) = True"
78 and_true: "(a & True) = a"
79 and_false: "(a & False) = False"
80 or_true: "(a | True) = True"
81 or_false: "(a | False) = a"
82 and_commute: "(a & b) = (b & a)"
83 or_commute: "(a | b) = (b | a)"
85 (*.should be in Rational.thy, but:
86 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
87 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
88 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
90 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
92 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
95 text {*copy from doc/math-eng.tex WN.28.3.03
98 section {*Coding standards*}
99 subsection {*Identifiers*}
100 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).
102 This are the preliminary rules for naming identifiers>
104 \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}.
105 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
106 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
107 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
111 %WN071228 extended *}
113 subsection {*Rule sets*}
114 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.
116 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.
119 \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).
121 \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.
123 \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.
124 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).
127 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.
128 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
136 {\tt append_rls, merge_rls, remove_rls} TODO
142 (** evaluation of numerals and special predicates on the meta-level **)
143 (*-------------------------functions---------------------*)
144 local (* rlang 09.02 *)
145 (*.a 'c is coefficient of v' if v does occur in c.*)
146 fun coeff_in v c = member op = (vars c) v;
148 fun occurs_in v t = coeff_in v t;
151 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
152 fun eval_occurs_in _ "Atools.occurs'_in"
153 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
154 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
155 writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
157 then SOME ((term2str p) ^ " = True",
158 Trueprop $ (mk_equality (p, HOLogic.true_const)))
159 else SOME ((term2str p) ^ " = False",
160 Trueprop $ (mk_equality (p, HOLogic.false_const))))
161 | eval_occurs_in _ _ _ _ = NONE;
163 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
164 fun some_occur_in vs t =
165 let fun occurs_in' a b = occurs_in b a
166 in foldl or_ (false, map (occurs_in' t) vs) end;
168 (*("some_occur_in", ("Atools.some'_occur'_in",
169 eval_some_occur_in "#eval_some_occur_in_"))*)
170 fun eval_some_occur_in _ "Atools.some'_occur'_in"
171 (p as (Const ("Atools.some'_occur'_in",_)
173 if some_occur_in (isalist2list vs) t
174 then SOME ((term2str p) ^ " = True",
175 Trueprop $ (mk_equality (p, HOLogic.true_const)))
176 else SOME ((term2str p) ^ " = False",
177 Trueprop $ (mk_equality (p, HOLogic.false_const)))
178 | eval_some_occur_in _ _ _ _ = NONE;
183 (*evaluate 'is_atom'*)
184 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
185 fun eval_is_atom (thmid:string) "Atools.is'_atom"
186 (t as (Const(op0,_) $ arg)) thy =
188 Free (n,_) => SOME (mk_thmid thmid op0 n "",
189 Trueprop $ (mk_equality (t, true_as_term)))
190 | _ => SOME (mk_thmid thmid op0 "" "",
191 Trueprop $ (mk_equality (t, false_as_term))))
192 | eval_is_atom _ _ _ _ = NONE;
194 (*evaluate 'is_even'*)
195 fun even i = (i div 2) * 2 = i;
196 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
197 fun eval_is_even (thmid:string) "Atools.is'_even"
198 (t as (Const(op0,_) $ arg)) thy =
201 (case int_of_str n of
203 if even i then SOME (mk_thmid thmid op0 n "",
204 Trueprop $ (mk_equality (t, true_as_term)))
205 else SOME (mk_thmid thmid op0 "" "",
206 Trueprop $ (mk_equality (t, false_as_term)))
209 | eval_is_even _ _ _ _ = NONE;
211 (*evaluate 'is_const'*)
212 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
213 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
214 (t as (Const(op0,t0) $ arg)) (thy:theory) =
215 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
218 SOME (mk_thmid thmid op0 n1 "",
219 Trueprop $ (mk_equality (t, false_as_term)))
222 then SOME (mk_thmid thmid op0 n1 "",
223 Trueprop $ (mk_equality (t, true_as_term)))
224 else SOME (mk_thmid thmid op0 n1 "",
225 Trueprop $ (mk_equality (t, false_as_term)))
226 | Const ("Float.Float",_) =>
227 SOME (mk_thmid thmid op0 (term2str arg) "",
228 Trueprop $ (mk_equality (t, true_as_term)))
230 SOME (mk_thmid thmid op0 (term2str arg) "",
231 Trueprop $ (mk_equality (t, false_as_term))))
232 | eval_const _ _ _ _ = NONE;
234 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
235 (*("PLUS" ,("op +" ,eval_binop "#add_")),
236 ("TIMES" ,("op *" ,eval_binop "#mult_")),
237 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
239 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
240 ("xxxxxx",op_,t,thy);
242 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
244 (string_of_int v11)^","^(string_of_int v12)^"), ("^
245 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
246 (string_of_int v21)^","^(string_of_int v22)^"), ("^
247 (string_of_int p21)^","^(string_of_int p22)^"))";
249 (*.convert int and float to internal floatingpoint prepresentation.*)
250 fun numeral (Free (str, T)) =
251 (case int_of_str str of
252 SOME i => SOME ((i, 0), (0, 0))
254 | numeral (Const ("Float.Float", _) $
256 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
257 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
258 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
259 (SOME v1', SOME v2', SOME p1', SOME p2') =>
260 SOME ((v1', v2'), (p1', p2'))
264 (*.evaluate binary associative operations.*)
265 fun eval_binop (thmid:string) (op_:string)
266 (t as ( Const(op0,t0) $
267 (Const(op0',t0') $ v $ t1) $ t2))
268 thy = (*binary . (v.n1).n2*)
270 case (numeral t1, numeral t2) of
271 (SOME n1, SOME n2) =>
272 let val (T1,T2,Trange) = dest_binop_typ t0
273 val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
274 (*WN071229 "HOL.divide" never tried*)
275 val rhs = var_op_float v op_ t0 T1 res
276 val prop = Trueprop $ (mk_equality (t, rhs))
277 in SOME (mk_thmid_f thmid n1 n2, prop) end
280 | eval_binop (thmid:string) (op_:string)
282 (Const (op0, t0) $ t1 $
283 (Const (op0', t0') $ t2 $ v)))
284 thy = (*binary . n1.(n2.v)*)
286 case (numeral t1, numeral t2) of
287 (SOME n1, SOME n2) =>
288 if op0 = "op -" then NONE else
289 let val (T1,T2,Trange) = dest_binop_typ t0
290 val res = calc op0 n1 n2
291 val rhs = float_op_var v op_ t0 T1 res
292 val prop = Trueprop $ (mk_equality (t, rhs))
293 in SOME (mk_thmid_f thmid n1 n2, prop) end
297 | eval_binop (thmid:string) (op_:string)
298 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
299 (case (numeral t1, numeral t2) of
300 (SOME n1, SOME n2) =>
301 let val (T1,T2,Trange) = dest_binop_typ t0;
302 val res = calc op0 n1 n2;
303 val rhs = term_of_float Trange res;
304 val prop = Trueprop $ (mk_equality (t, rhs));
305 in SOME (mk_thmid_f thmid n1 n2, prop) end
307 | eval_binop _ _ _ _ = NONE;
309 > val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
311 val it = "-1 + 2 = 1"
312 > val t = str2term "-1 * (-1 * a)";
313 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
315 val it = "-1 * (-1 * a) = 1 * a"*)
319 (*.evaluate < and <= for numerals.*)
320 (*("le" ,("op <" ,eval_equ "#less_")),
321 ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
322 fun eval_equ (thmid:string) (op_:string) (t as
323 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
324 (case (int_of_str n1, int_of_str n2) of
325 (SOME n1', SOME n2') =>
326 if calc_equ (strip_thy op0) (n1', n2')
327 then SOME (mk_thmid thmid op0 n1 n2,
328 Trueprop $ (mk_equality (t, true_as_term)))
329 else SOME (mk_thmid thmid op0 n1 n2,
330 Trueprop $ (mk_equality (t, false_as_term)))
333 | eval_equ _ _ _ _ = NONE;
338 val it = "(?t = ?t) = True"
339 > val t = str2term "x = 0";
340 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
342 > val t = str2term "1 = 0";
343 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
344 ----------- thus needs Calc !
345 > val t = str2term "0 = 0";
346 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
350 val t = str2term "Not (x = 0)";
357 val it = "x ~= 0" : string*)
359 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
360 the arguments: thus special handling by 'fun eval_binop'*)
361 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
362 fun eval_ident (thmid:string) "Atools.ident" (t as
363 (Const (op0,t0) $ t1 $ t2 )) thy =
365 then SOME (mk_thmid thmid op0
366 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
367 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
368 Trueprop $ (mk_equality (t, true_as_term)))
369 else SOME (mk_thmid thmid op0
370 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
371 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
372 Trueprop $ (mk_equality (t, false_as_term)))
373 | eval_ident _ _ _ _ = NONE;
375 > val t = str2term "x =!= 0";
376 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
378 val str = "ident_(x)_(0)" : string
379 val it = "(x =!= 0) = False" : string
380 > val t = str2term "1 =!= 0";
381 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
383 val str = "ident_(1)_(0)" : string
384 val it = "(1 =!= 0) = False" : string
385 > val t = str2term "0 =!= 0";
386 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
388 val str = "ident_(0)_(0)" : string
389 val it = "(0 =!= 0) = True" : string
392 (*.evaluate identity of terms, which stay ready for evaluation in turn;
393 thus returns False only for atoms.*)
394 (*("equal" ,("op =",eval_equal "#equal_")):calc*)
395 fun eval_equal (thmid:string) "op =" (t as
396 (Const (op0,t0) $ t1 $ t2 )) thy =
398 then ((*writeln"... eval_equal: t1 = t2 --> True";*)
399 SOME (mk_thmid thmid op0
400 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
401 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
402 Trueprop $ (mk_equality (t, true_as_term)))
404 else (case (is_atom t1, is_atom t2) of
406 ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
407 SOME (mk_thmid thmid op0
408 ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
409 Trueprop $ (mk_equality (t, false_as_term)))
411 | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
413 | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
416 val t = str2term "x ~= 0";
417 val NONE = eval_equal "equal_" "b" t thy;
420 > val t = str2term "(x + 1) = (x + 1)";
421 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
423 val str = "equal_(x + 1)_(x + 1)" : string
424 val it = "(x + 1 = x + 1) = True" : string
425 > val t = str2term "x = 0";
426 > val NONE = eval_equal "equal_" "b" t thy;
428 > val t = str2term "1 = 0";
429 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
431 val str = "equal_(1)_(0)" : string
432 val it = "(1 = 0) = False" : string
433 > val t = str2term "0 = 0";
434 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
436 val str = "equal_(0)_(0)" : string
437 val it = "(0 = 0) = True" : string
441 (** evaluation on the metalevel **)
443 (*. evaluate HOL.divide .*)
444 (*("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e"))*)
445 fun eval_cancel (thmid:string) "HOL.divide" (t as
446 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
447 (case (int_of_str n1, int_of_str n2) of
448 (SOME n1', SOME n2') =>
450 val sg = sign2 n1' n2';
451 val (T1,T2,Trange) = dest_binop_typ t0;
452 val gcd' = gcd (abs n1') (abs n2');
454 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
455 val prop = Trueprop $ (mk_equality (t, rhs))
456 in SOME (mk_thmid thmid op0 n1 n2, prop) end
457 else if 0 < n2' andalso gcd' = 1 then NONE
458 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
460 val prop = Trueprop $ (mk_equality (t, rhs))
461 in SOME (mk_thmid thmid op0 n1 n2, prop) end
463 | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
465 | eval_cancel _ _ _ _ = NONE;
467 (*. get the argument from a function-definition.*)
468 (*("argument_in" ,("Atools.argument'_in",
469 eval_argument_in "Atools.argument'_in"))*)
470 fun eval_argument_in _ "Atools.argument'_in"
471 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
472 if is_Free arg (*could be something to be simplified before*)
473 then SOME (term2str t ^ " = " ^ term2str arg,
474 Trueprop $ (mk_equality (t, arg)))
476 | eval_argument_in _ _ _ _ = NONE;
478 (*.check if the function-identifier of the first argument matches
479 the function-identifier of the lhs of the second argument.*)
480 (*("sameFunId" ,("Atools.sameFunId",
481 eval_same_funid "Atools.sameFunId"))*)
482 fun eval_sameFunId _ "Atools.sameFunId"
483 (p as Const ("Atools.sameFunId",_) $
485 (Const ("op =", _) $ (f2 $ _) $ _)) _ =
487 then SOME ((term2str p) ^ " = True",
488 Trueprop $ (mk_equality (p, HOLogic.true_const)))
489 else SOME ((term2str p) ^ " = False",
490 Trueprop $ (mk_equality (p, HOLogic.false_const)))
491 | eval_sameFunId _ _ _ _ = NONE;
494 (*.from a list of fun-definitions "f x = ..." as 2nd argument
495 filter the elements with the same fun-identfier in "f y"
497 this is, because Isabelles filter takes more than 1 sec.*)
498 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
499 | same_funid f1 t = raise error ("same_funid called with t = ("
500 ^term2str f1^") ("^term2str t^")");
501 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
502 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
503 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
504 (p as Const ("Atools.filter'_sameFunId",_) $
506 let val fs' = ((list2isalist HOLogic.boolT) o
507 (filter (same_funid fid))) (isalist2list fs)
508 in SOME (term2str (mk_equality (p, fs')),
509 Trueprop $ (mk_equality (p, fs'))) end
510 | eval_filter_sameFunId _ _ _ _ = NONE;
513 (*make a list of terms to a sum*)
514 fun list2sum [] = error ("list2sum called with []")
517 let fun sum su [s'] =
518 Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
521 sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
525 (*make a list of equalities to the sum of the lhs*)
526 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
527 fun eval_boollist2sum _ "Atools.boollist2sum"
528 (p as Const ("Atools.boollist2sum", _) $
529 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
530 let val isal = isalist2list l
531 val lhss = map lhs isal
532 val sum = list2sum lhss
533 in SOME ((term2str p) ^ " = " ^ (term2str sum),
534 Trueprop $ (mk_equality (p, sum)))
536 | eval_boollist2sum _ _ _ _ = NONE;
545 fun termlessI (_:subst) uv = Term_Ord.termless uv;
546 fun term_ordI (_:subst) uv = Term_Ord.term_ord uv;
550 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
554 append_rls "list_rls" list_rls
555 [Calc ("op *",eval_binop "#mult_"),
556 Calc ("op +", eval_binop "#add_"),
557 Calc ("op <",eval_equ "#less_"),
558 Calc ("op <=",eval_equ "#less_equal_"),
559 Calc ("Atools.ident",eval_ident "#ident_"),
560 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
562 Calc ("Tools.Vars",eval_var "#Vars_"),
564 Thm ("if_True",num_str @{thm if_True}),
565 Thm ("if_False",num_str @{thm if_False})
568 ruleset' := overwritelthy thy (!ruleset',
569 [("list_rls",list_rls)
572 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
573 val tless_true = dummy_ord;
574 rew_ord' := overwritel (!rew_ord',
575 [("tless_true", tless_true),
576 ("e_rew_ord'", tless_true),
577 ("dummy_ord", dummy_ord)]);
579 val calculate_Atools =
580 append_rls "calculate_Atools" e_rls
581 [Calc ("op <",eval_equ "#less_"),
582 Calc ("op <=",eval_equ "#less_equal_"),
583 Calc ("op =",eval_equal "#equal_"),
585 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
586 Calc ("op +",eval_binop "#add_"),
587 Calc ("op -",eval_binop "#sub_"),
588 Calc ("op *",eval_binop "#mult_")
592 append_rls "Atools_erls" e_rls
593 [Calc ("op =",eval_equal "#equal_"),
594 Thm ("not_true",num_str @{thm not_true}),
595 (*"(~ True) = False"*)
596 Thm ("not_false",num_str @{thm not_false}),
597 (*"(~ False) = True"*)
598 Thm ("and_true",num_str @{thm and_true}),
599 (*"(?a & True) = ?a"*)
600 Thm ("and_false",num_str @{thm and_false}),
601 (*"(?a & False) = False"*)
602 Thm ("or_true",num_str @{thm or_true}),
603 (*"(?a | True) = True"*)
604 Thm ("or_false",num_str @{thm or_false}),
605 (*"(?a | False) = ?a"*)
607 Thm ("rat_leq1",num_str @{thm rat_leq1}),
608 Thm ("rat_leq2",num_str @{thm rat_leq2}),
609 Thm ("rat_leq3",num_str @{thm rat_leq3}),
610 Thm ("refl",num_str @{thm refl}),
611 Thm ("real_le_refl",num_str @{thm real_le_refl}),
612 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
614 Calc ("op <",eval_equ "#less_"),
615 Calc ("op <=",eval_equ "#less_equal_"),
617 Calc ("Atools.ident",eval_ident "#ident_"),
618 Calc ("Atools.is'_const",eval_const "#is_const_"),
619 Calc ("Atools.occurs'_in",eval_occurs_in ""),
620 Calc ("Tools.matches",eval_matches "")
624 append_rls "Atools_crls" e_rls
625 [Calc ("op =",eval_equal "#equal_"),
626 Thm ("not_true",num_str @{thm not_true}),
627 Thm ("not_false",num_str @{thm not_false}),
628 Thm ("and_true",num_str @{thm and_true}),
629 Thm ("and_false",num_str @{thm and_false}),
630 Thm ("or_true",num_str @{thm or_true}),
631 Thm ("or_false",num_str @{thm or_false}),
633 Thm ("rat_leq1",num_str @{thm rat_leq1}),
634 Thm ("rat_leq2",num_str @{thm rat_leq2}),
635 Thm ("rat_leq3",num_str @{thm rat_leq3}),
636 Thm ("refl",num_str @{thm refl}),
637 Thm ("real_le_refl",num_str @{thm real_le_refl}),
638 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
640 Calc ("op <",eval_equ "#less_"),
641 Calc ("op <=",eval_equ "#less_equal_"),
643 Calc ("Atools.ident",eval_ident "#ident_"),
644 Calc ("Atools.is'_const",eval_const "#is_const_"),
645 Calc ("Atools.occurs'_in",eval_occurs_in ""),
646 Calc ("Tools.matches",eval_matches "")
649 (*val atools_erls = ... waere zu testen ...
650 merge_rls calculate_Atools
651 (append_rls Atools_erls (*i.A. zu viele rules*)
652 [Calc ("Atools.ident",eval_ident "#ident_"),
653 Calc ("Atools.is'_const",eval_const "#is_const_"),
654 Calc ("Atools.occurs'_in",
655 eval_occurs_in "#occurs_in"),
656 Calc ("Tools.matches",eval_matches "#matches")
657 ] (*i.A. zu viele rules*)
659 (* val atools_erls = prep_rls(
660 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
661 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
662 rules = [Thm ("refl",num_str @{thm refl}),
663 Thm ("real_le_refl",num_str @{thm real_le_refl}),
664 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
665 Thm ("not_true",num_str @{thm not_true}),
666 Thm ("not_false",num_str @{thm not_false}),
667 Thm ("and_true",num_str @{thm and_true}),
668 Thm ("and_false",num_str @{thm and_false}),
669 Thm ("or_true",num_str @{thm or_true}),
670 Thm ("or_false",num_str @{thm or_false}),
671 Thm ("and_commute",num_str @{thm and_commute}),
672 Thm ("or_commute",num_str @{thm or_commute}),
674 Calc ("op <",eval_equ "#less_"),
675 Calc ("op <=",eval_equ "#less_equal_"),
677 Calc ("Atools.ident",eval_ident "#ident_"),
678 Calc ("Atools.is'_const",eval_const "#is_const_"),
679 Calc ("Atools.occurs'_in",eval_occurs_in ""),
680 Calc ("Tools.matches",eval_matches "")
682 scr = Script ((term_of o the o (parse @{theory}))
685 ruleset' := overwritelth @{theory}
687 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
690 "******* Atools.ML end *******";
692 calclist':= overwritel (!calclist',
693 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
695 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
696 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
697 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
698 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
699 ("le" ,("op <" ,eval_equ "#less_")),
700 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
701 ("ident" ,("Atools.ident",eval_ident "#ident_")),
702 ("equal" ,("op =",eval_equal "#equal_")),
703 ("PLUS" ,("op +" ,eval_binop "#add_")),
704 ("MINUS" ,("op -",eval_binop "#sub_")),
705 ("TIMES" ,("op *" ,eval_binop "#mult_")),
706 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
707 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
708 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
711 val list_rls = prep_rls(
712 merge_rls "list_erls"
713 (Rls {id="replaced",preconds = [],
714 rew_ord = ("termlessI", termlessI),
715 erls = Rls {id="list_elrs", preconds = [],
716 rew_ord = ("termlessI",termlessI),
718 srls = Erls, calc = [], (*asm_thm = [],*)
719 rules = [Calc ("op +", eval_binop "#add_"),
720 Calc ("op <",eval_equ "#less_")
721 (* ~~~~~~ for nth_Cons_*)
724 srls = Erls, calc = [], (*asm_thm = [], *)
725 rules = [], scr = EmptyScr})
727 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);