updated Knowledge/Equation.thy, plus changes ahead.
find . -type f -exec sed -i s/' e_\"'/' e_e\"'/g {} \;
find . -type f -exec sed -i s/' e_ '/' e_e '/g {} \;
find . -type f -exec sed -i s/' e_)'/' e_e)'/g {} \;
find . -type f -exec sed -i s/' e_,'/' e_e,'/g {} \;
find . -type f -exec sed -i s/' e_:'/' e_e:'/g {} \;
find . -type f -exec sed -i s/'(e_:'/'(e_e:'/g {} \;
find . -type f -exec sed -i s/' v_\"'/' v_v\"'/g {} \;
find . -type f -exec sed -i s/' v_ '/' v_v '/g {} \;
find . -type f -exec sed -i s/' v_)'/' v_v)'/g {} \;
find . -type f -exec sed -i s/' v_,'/' v_v,'/g {} \;
find . -type f -exec sed -i s/' v_:'/' v_v:'/g {} \;
find . -type f -exec sed -i s/' v_i\"'/' v_i\"'/g {} \;
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")
16 use "Interpret/mstools.sml"
17 use "Interpret/ctree.sml"
18 use "Interpret/ptyps.sml" (*^^^ need files for: fun prep_pbt, fun store_pbt*)
19 use "Interpret/generate.sml"
20 use "Interpret/calchead.sml"
21 use "Interpret/appl.sml"
22 use "Interpret/rewtools.sml"
23 use "Interpret/script.sml"
24 use "Interpret/solve.sml"
25 use "Interpret/inform.sml" (*^^^ need files for: fun castab*)
26 use "Interpret/mathengine.sml"
34 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
35 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
37 pow :: "[real, real] => real" (infixr "^^^" 80)
38 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
40 (*WN0603 at FE-interface encoded strings to '^',
41 see 'fun encode', fun 'decode'*)
43 abs :: "real => real" ("(|| _ ||)")
44 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
45 absset :: "real set => real" ("(||| _ |||)")
46 (*is numeral constant ?*)
47 is'_const :: "real => bool" ("_ is'_const" 10)
48 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
49 is'_atom :: "real => bool" ("_ is'_atom" 10)
50 is'_even :: "real => bool" ("_ is'_even" 10)
52 (* identity on term level*)
53 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
55 argument'_in :: "real => real" ("argument'_in _" 10)
56 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
57 WN0609 changed the id, because ".. _ _" inhibits currying**)
58 filter'_sameFunId:: "[real, bool list] => bool list"
59 ("filter'_sameFunId _ _" 10)
60 boollist2sum :: "bool list => real"
62 axioms (*for evaluating the assumptions of conditional rules*)
64 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
65 real_unari_minus: "- a = (-1) * a"
67 rle_refl: "(n::real) <= n"
68 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
69 not_true: "(~ True) = False"
70 not_false: "(~ False) = True"
71 and_true: "(a & True) = a"
72 and_false: "(a & False) = False"
73 or_true: "(a | True) = True"
74 or_false: "(a | False) = a"
75 and_commute: "(a & b) = (b & a)"
76 or_commute: "(a | b) = (b | a)"
78 (*.should be in Rational.thy, but:
79 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
80 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
81 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
83 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
85 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
88 text {*copy from doc/math-eng.tex WN.28.3.03
91 section {*Coding standards*}
92 subsection {*Identifiers*}
93 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).
95 This are the preliminary rules for naming identifiers>
97 \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}.
98 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
99 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
100 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
104 %WN071228 extended *}
106 subsection {*Rule sets*}
107 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.
109 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.
112 \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).
114 \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.
116 \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.
117 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).
120 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.
121 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
129 {\tt append_rls, merge_rls, remove_rls} TODO
135 (** evaluation of numerals and special predicates on the meta-level **)
136 (*-------------------------functions---------------------*)
137 local (* rlang 09.02 *)
138 (*.a 'c is coefficient of v' if v does occur in c.*)
139 fun coeff_in v c = member op = (vars c) v;
141 fun occurs_in v t = coeff_in v t;
144 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
145 fun eval_occurs_in _ "Atools.occurs'_in"
146 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
147 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
148 writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
150 then SOME ((term2str p) ^ " = True",
151 Trueprop $ (mk_equality (p, HOLogic.true_const)))
152 else SOME ((term2str p) ^ " = False",
153 Trueprop $ (mk_equality (p, HOLogic.false_const))))
154 | eval_occurs_in _ _ _ _ = NONE;
156 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
157 fun some_occur_in vs t =
158 let fun occurs_in' a b = occurs_in b a
159 in foldl or_ (false, map (occurs_in' t) vs) end;
161 (*("some_occur_in", ("Atools.some'_occur'_in",
162 eval_some_occur_in "#eval_some_occur_in_"))*)
163 fun eval_some_occur_in _ "Atools.some'_occur'_in"
164 (p as (Const ("Atools.some'_occur'_in",_)
166 if some_occur_in (isalist2list vs) t
167 then SOME ((term2str p) ^ " = True",
168 Trueprop $ (mk_equality (p, HOLogic.true_const)))
169 else SOME ((term2str p) ^ " = False",
170 Trueprop $ (mk_equality (p, HOLogic.false_const)))
171 | eval_some_occur_in _ _ _ _ = NONE;
176 (*evaluate 'is_atom'*)
177 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
178 fun eval_is_atom (thmid:string) "Atools.is'_atom"
179 (t as (Const(op0,_) $ arg)) thy =
181 Free (n,_) => SOME (mk_thmid thmid op0 n "",
182 Trueprop $ (mk_equality (t, true_as_term)))
183 | _ => SOME (mk_thmid thmid op0 "" "",
184 Trueprop $ (mk_equality (t, false_as_term))))
185 | eval_is_atom _ _ _ _ = NONE;
187 (*evaluate 'is_even'*)
188 fun even i = (i div 2) * 2 = i;
189 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
190 fun eval_is_even (thmid:string) "Atools.is'_even"
191 (t as (Const(op0,_) $ arg)) thy =
194 (case int_of_str n of
196 if even i then SOME (mk_thmid thmid op0 n "",
197 Trueprop $ (mk_equality (t, true_as_term)))
198 else SOME (mk_thmid thmid op0 "" "",
199 Trueprop $ (mk_equality (t, false_as_term)))
202 | eval_is_even _ _ _ _ = NONE;
204 (*evaluate 'is_const'*)
205 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
206 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
207 (t as (Const(op0,t0) $ arg)) (thy:theory) =
208 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
211 SOME (mk_thmid thmid op0 n1 "",
212 Trueprop $ (mk_equality (t, false_as_term)))
215 then SOME (mk_thmid thmid op0 n1 "",
216 Trueprop $ (mk_equality (t, true_as_term)))
217 else SOME (mk_thmid thmid op0 n1 "",
218 Trueprop $ (mk_equality (t, false_as_term)))
219 | Const ("Float.Float",_) =>
220 SOME (mk_thmid thmid op0 (term2str arg) "",
221 Trueprop $ (mk_equality (t, true_as_term)))
223 SOME (mk_thmid thmid op0 (term2str arg) "",
224 Trueprop $ (mk_equality (t, false_as_term))))
225 | eval_const _ _ _ _ = NONE;
227 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
228 (*("PLUS" ,("op +" ,eval_binop "#add_")),
229 ("TIMES" ,("op *" ,eval_binop "#mult_")),
230 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
232 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
233 ("xxxxxx",op_,t,thy);
235 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
237 (string_of_int v11)^","^(string_of_int v12)^"), ("^
238 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
239 (string_of_int v21)^","^(string_of_int v22)^"), ("^
240 (string_of_int p21)^","^(string_of_int p22)^"))";
242 (*.convert int and float to internal floatingpoint prepresentation.*)
243 fun numeral (Free (str, T)) =
244 (case int_of_str str of
245 SOME i => SOME ((i, 0), (0, 0))
247 | numeral (Const ("Float.Float", _) $
249 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
250 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
251 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
252 (SOME v1', SOME v2', SOME p1', SOME p2') =>
253 SOME ((v1', v2'), (p1', p2'))
257 (*.evaluate binary associative operations.*)
258 fun eval_binop (thmid:string) (op_:string)
259 (t as ( Const(op0,t0) $
260 (Const(op0',t0') $ v $ t1) $ t2))
261 thy = (*binary . (v.n1).n2*)
263 case (numeral t1, numeral t2) of
264 (SOME n1, SOME n2) =>
265 let val (T1,T2,Trange) = dest_binop_typ t0
266 val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
267 (*WN071229 "HOL.divide" never tried*)
268 val rhs = var_op_float v op_ t0 T1 res
269 val prop = Trueprop $ (mk_equality (t, rhs))
270 in SOME (mk_thmid_f thmid n1 n2, prop) end
273 | eval_binop (thmid:string) (op_:string)
275 (Const (op0, t0) $ t1 $
276 (Const (op0', t0') $ t2 $ v)))
277 thy = (*binary . n1.(n2.v)*)
279 case (numeral t1, numeral t2) of
280 (SOME n1, SOME n2) =>
281 if op0 = "op -" then NONE else
282 let val (T1,T2,Trange) = dest_binop_typ t0
283 val res = calc op0 n1 n2
284 val rhs = float_op_var v op_ t0 T1 res
285 val prop = Trueprop $ (mk_equality (t, rhs))
286 in SOME (mk_thmid_f thmid n1 n2, prop) end
290 | eval_binop (thmid:string) (op_:string)
291 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
292 (case (numeral t1, numeral t2) of
293 (SOME n1, SOME n2) =>
294 let val (T1,T2,Trange) = dest_binop_typ t0;
295 val res = calc op0 n1 n2;
296 val rhs = term_of_float Trange res;
297 val prop = Trueprop $ (mk_equality (t, rhs));
298 in SOME (mk_thmid_f thmid n1 n2, prop) end
300 | eval_binop _ _ _ _ = NONE;
302 > val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
304 val it = "-1 + 2 = 1"
305 > val t = str2term "-1 * (-1 * a)";
306 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
308 val it = "-1 * (-1 * a) = 1 * a"*)
312 (*.evaluate < and <= for numerals.*)
313 (*("le" ,("op <" ,eval_equ "#less_")),
314 ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
315 fun eval_equ (thmid:string) (op_:string) (t as
316 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
317 (case (int_of_str n1, int_of_str n2) of
318 (SOME n1', SOME n2') =>
319 if calc_equ (strip_thy op0) (n1', n2')
320 then SOME (mk_thmid thmid op0 n1 n2,
321 Trueprop $ (mk_equality (t, true_as_term)))
322 else SOME (mk_thmid thmid op0 n1 n2,
323 Trueprop $ (mk_equality (t, false_as_term)))
326 | eval_equ _ _ _ _ = NONE;
331 val it = "(?t = ?t) = True"
332 > val t = str2term "x = 0";
333 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
335 > val t = str2term "1 = 0";
336 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
337 ----------- thus needs Calc !
338 > val t = str2term "0 = 0";
339 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
343 val t = str2term "Not (x = 0)";
350 val it = "x ~= 0" : string*)
352 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
353 the arguments: thus special handling by 'fun eval_binop'*)
354 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
355 fun eval_ident (thmid:string) "Atools.ident" (t as
356 (Const (op0,t0) $ t1 $ t2 )) thy =
358 then SOME (mk_thmid thmid op0
359 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
360 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
361 Trueprop $ (mk_equality (t, true_as_term)))
362 else SOME (mk_thmid thmid op0
363 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
364 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
365 Trueprop $ (mk_equality (t, false_as_term)))
366 | eval_ident _ _ _ _ = NONE;
368 > val t = str2term "x =!= 0";
369 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
371 val str = "ident_(x)_(0)" : string
372 val it = "(x =!= 0) = False" : string
373 > val t = str2term "1 =!= 0";
374 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
376 val str = "ident_(1)_(0)" : string
377 val it = "(1 =!= 0) = False" : string
378 > val t = str2term "0 =!= 0";
379 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
381 val str = "ident_(0)_(0)" : string
382 val it = "(0 =!= 0) = True" : string
385 (*.evaluate identity of terms, which stay ready for evaluation in turn;
386 thus returns False only for atoms.*)
387 (*("equal" ,("op =",eval_equal "#equal_")):calc*)
388 fun eval_equal (thmid:string) "op =" (t as
389 (Const (op0,t0) $ t1 $ t2 )) thy =
391 then ((*writeln"... eval_equal: t1 = t2 --> True";*)
392 SOME (mk_thmid thmid op0
393 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
394 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
395 Trueprop $ (mk_equality (t, true_as_term)))
397 else (case (is_atom t1, is_atom t2) of
399 ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
400 SOME (mk_thmid thmid op0
401 ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
402 Trueprop $ (mk_equality (t, false_as_term)))
404 | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
406 | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
409 val t = str2term "x ~= 0";
410 val NONE = eval_equal "equal_" "b" t thy;
413 > val t = str2term "(x + 1) = (x + 1)";
414 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
416 val str = "equal_(x + 1)_(x + 1)" : string
417 val it = "(x + 1 = x + 1) = True" : string
418 > val t = str2term "x = 0";
419 > val NONE = eval_equal "equal_" "b" t thy;
421 > val t = str2term "1 = 0";
422 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
424 val str = "equal_(1)_(0)" : string
425 val it = "(1 = 0) = False" : string
426 > val t = str2term "0 = 0";
427 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
429 val str = "equal_(0)_(0)" : string
430 val it = "(0 = 0) = True" : string
434 (** evaluation on the metalevel **)
436 (*. evaluate HOL.divide .*)
437 (*("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e"))*)
438 fun eval_cancel (thmid:string) "HOL.divide" (t as
439 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
440 (case (int_of_str n1, int_of_str n2) of
441 (SOME n1', SOME n2') =>
443 val sg = sign2 n1' n2';
444 val (T1,T2,Trange) = dest_binop_typ t0;
445 val gcd' = gcd (abs n1') (abs n2');
447 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
448 val prop = Trueprop $ (mk_equality (t, rhs))
449 in SOME (mk_thmid thmid op0 n1 n2, prop) end
450 else if 0 < n2' andalso gcd' = 1 then NONE
451 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
453 val prop = Trueprop $ (mk_equality (t, rhs))
454 in SOME (mk_thmid thmid op0 n1 n2, prop) end
456 | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
458 | eval_cancel _ _ _ _ = NONE;
460 (*. get the argument from a function-definition.*)
461 (*("argument_in" ,("Atools.argument'_in",
462 eval_argument_in "Atools.argument'_in"))*)
463 fun eval_argument_in _ "Atools.argument'_in"
464 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
465 if is_Free arg (*could be something to be simplified before*)
466 then SOME (term2str t ^ " = " ^ term2str arg,
467 Trueprop $ (mk_equality (t, arg)))
469 | eval_argument_in _ _ _ _ = NONE;
471 (*.check if the function-identifier of the first argument matches
472 the function-identifier of the lhs of the second argument.*)
473 (*("sameFunId" ,("Atools.sameFunId",
474 eval_same_funid "Atools.sameFunId"))*)
475 fun eval_sameFunId _ "Atools.sameFunId"
476 (p as Const ("Atools.sameFunId",_) $
478 (Const ("op =", _) $ (f2 $ _) $ _)) _ =
480 then SOME ((term2str p) ^ " = True",
481 Trueprop $ (mk_equality (p, HOLogic.true_const)))
482 else SOME ((term2str p) ^ " = False",
483 Trueprop $ (mk_equality (p, HOLogic.false_const)))
484 | eval_sameFunId _ _ _ _ = NONE;
487 (*.from a list of fun-definitions "f x = ..." as 2nd argument
488 filter the elements with the same fun-identfier in "f y"
490 this is, because Isabelles filter takes more than 1 sec.*)
491 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
492 | same_funid f1 t = raise error ("same_funid called with t = ("
493 ^term2str f1^") ("^term2str t^")");
494 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
495 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
496 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
497 (p as Const ("Atools.filter'_sameFunId",_) $
499 let val fs' = ((list2isalist HOLogic.boolT) o
500 (filter (same_funid fid))) (isalist2list fs)
501 in SOME (term2str (mk_equality (p, fs')),
502 Trueprop $ (mk_equality (p, fs'))) end
503 | eval_filter_sameFunId _ _ _ _ = NONE;
506 (*make a list of terms to a sum*)
507 fun list2sum [] = error ("list2sum called with []")
510 let fun sum su [s'] =
511 Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
514 sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
518 (*make a list of equalities to the sum of the lhs*)
519 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
520 fun eval_boollist2sum _ "Atools.boollist2sum"
521 (p as Const ("Atools.boollist2sum", _) $
522 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
523 let val isal = isalist2list l
524 val lhss = map lhs isal
525 val sum = list2sum lhss
526 in SOME ((term2str p) ^ " = " ^ (term2str sum),
527 Trueprop $ (mk_equality (p, sum)))
529 | eval_boollist2sum _ _ _ _ = NONE;
538 fun termlessI (_:subst) uv = Term_Ord.termless uv;
539 fun term_ordI (_:subst) uv = Term_Ord.term_ord uv;
543 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
547 append_rls "list_rls" list_rls
548 [Calc ("op *",eval_binop "#mult_"),
549 Calc ("op +", eval_binop "#add_"),
550 Calc ("op <",eval_equ "#less_"),
551 Calc ("op <=",eval_equ "#less_equal_"),
552 Calc ("Atools.ident",eval_ident "#ident_"),
553 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
555 Calc ("Tools.Vars",eval_var "#Vars_"),
557 Thm ("if_True",num_str @{thm if_True}),
558 Thm ("if_False",num_str @{thm if_False})
561 ruleset' := overwritelthy thy (!ruleset',
562 [("list_rls",list_rls)
565 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
566 val tless_true = dummy_ord;
567 rew_ord' := overwritel (!rew_ord',
568 [("tless_true", tless_true),
569 ("e_rew_ord'", tless_true),
570 ("dummy_ord", dummy_ord)]);
572 val calculate_Atools =
573 append_rls "calculate_Atools" e_rls
574 [Calc ("op <",eval_equ "#less_"),
575 Calc ("op <=",eval_equ "#less_equal_"),
576 Calc ("op =",eval_equal "#equal_"),
578 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
579 Calc ("op +",eval_binop "#add_"),
580 Calc ("op -",eval_binop "#sub_"),
581 Calc ("op *",eval_binop "#mult_")
585 append_rls "Atools_erls" e_rls
586 [Calc ("op =",eval_equal "#equal_"),
587 Thm ("not_true",num_str @{thm not_true}),
588 (*"(~ True) = False"*)
589 Thm ("not_false",num_str @{thm not_false}),
590 (*"(~ False) = True"*)
591 Thm ("and_true",num_str @{thm and_true}),
592 (*"(?a & True) = ?a"*)
593 Thm ("and_false",num_str @{thm and_false}),
594 (*"(?a & False) = False"*)
595 Thm ("or_true",num_str @{thm or_true}),
596 (*"(?a | True) = True"*)
597 Thm ("or_false",num_str @{thm or_false}),
598 (*"(?a | False) = ?a"*)
600 Thm ("rat_leq1",num_str @{thm rat_leq1}),
601 Thm ("rat_leq2",num_str @{thm rat_leq2}),
602 Thm ("rat_leq3",num_str @{thm rat_leq3}),
603 Thm ("refl",num_str @{thm refl}),
604 Thm ("real_le_refl",num_str @{thm real_le_refl}),
605 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
607 Calc ("op <",eval_equ "#less_"),
608 Calc ("op <=",eval_equ "#less_equal_"),
610 Calc ("Atools.ident",eval_ident "#ident_"),
611 Calc ("Atools.is'_const",eval_const "#is_const_"),
612 Calc ("Atools.occurs'_in",eval_occurs_in ""),
613 Calc ("Tools.matches",eval_matches "")
617 append_rls "Atools_crls" e_rls
618 [Calc ("op =",eval_equal "#equal_"),
619 Thm ("not_true",num_str @{thm not_true}),
620 Thm ("not_false",num_str @{thm not_false}),
621 Thm ("and_true",num_str @{thm and_true}),
622 Thm ("and_false",num_str @{thm and_false}),
623 Thm ("or_true",num_str @{thm or_true}),
624 Thm ("or_false",num_str @{thm or_false}),
626 Thm ("rat_leq1",num_str @{thm rat_leq1}),
627 Thm ("rat_leq2",num_str @{thm rat_leq2}),
628 Thm ("rat_leq3",num_str @{thm rat_leq3}),
629 Thm ("refl",num_str @{thm refl}),
630 Thm ("real_le_refl",num_str @{thm real_le_refl}),
631 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
633 Calc ("op <",eval_equ "#less_"),
634 Calc ("op <=",eval_equ "#less_equal_"),
636 Calc ("Atools.ident",eval_ident "#ident_"),
637 Calc ("Atools.is'_const",eval_const "#is_const_"),
638 Calc ("Atools.occurs'_in",eval_occurs_in ""),
639 Calc ("Tools.matches",eval_matches "")
642 (*val atools_erls = ... waere zu testen ...
643 merge_rls calculate_Atools
644 (append_rls Atools_erls (*i.A. zu viele rules*)
645 [Calc ("Atools.ident",eval_ident "#ident_"),
646 Calc ("Atools.is'_const",eval_const "#is_const_"),
647 Calc ("Atools.occurs'_in",
648 eval_occurs_in "#occurs_in"),
649 Calc ("Tools.matches",eval_matches "#matches")
650 ] (*i.A. zu viele rules*)
652 (* val atools_erls = prep_rls(
653 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
654 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
655 rules = [Thm ("refl",num_str @{thm refl}),
656 Thm ("real_le_refl",num_str @{thm real_le_refl}),
657 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
658 Thm ("not_true",num_str @{thm not_true}),
659 Thm ("not_false",num_str @{thm not_false}),
660 Thm ("and_true",num_str @{thm and_true}),
661 Thm ("and_false",num_str @{thm and_false}),
662 Thm ("or_true",num_str @{thm or_true}),
663 Thm ("or_false",num_str @{thm or_false}),
664 Thm ("and_commute",num_str @{thm and_commute}),
665 Thm ("or_commute",num_str @{thm or_commute}),
667 Calc ("op <",eval_equ "#less_"),
668 Calc ("op <=",eval_equ "#less_equal_"),
670 Calc ("Atools.ident",eval_ident "#ident_"),
671 Calc ("Atools.is'_const",eval_const "#is_const_"),
672 Calc ("Atools.occurs'_in",eval_occurs_in ""),
673 Calc ("Tools.matches",eval_matches "")
675 scr = Script ((term_of o the o (parse @{theory}))
678 ruleset' := overwritelth @{theory}
680 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
683 "******* Atools.ML end *******";
685 calclist':= overwritel (!calclist',
686 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
688 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
689 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
690 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
691 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
692 ("le" ,("op <" ,eval_equ "#less_")),
693 ("leq" ,("op <=" ,eval_equ "#less_equal_")),
694 ("ident" ,("Atools.ident",eval_ident "#ident_")),
695 ("equal" ,("op =",eval_equal "#equal_")),
696 ("PLUS" ,("op +" ,eval_binop "#add_")),
697 ("MINUS" ,("op -",eval_binop "#sub_")),
698 ("TIMES" ,("op *" ,eval_binop "#mult_")),
699 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
700 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
701 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
704 val list_rls = prep_rls(
705 merge_rls "list_erls"
706 (Rls {id="replaced",preconds = [],
707 rew_ord = ("termlessI", termlessI),
708 erls = Rls {id="list_elrs", preconds = [],
709 rew_ord = ("termlessI",termlessI),
711 srls = Erls, calc = [], (*asm_thm = [],*)
712 rules = [Calc ("op +", eval_binop "#add_"),
713 Calc ("op <",eval_equ "#less_")
714 (* ~~~~~~ for nth_Cons_*)
717 srls = Erls, calc = [], (*asm_thm = [], *)
718 rules = [], scr = EmptyScr})
720 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);