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"
11 uses ("../Interpret/mstools.sml")("../Interpret/ctree.sml")
12 ("../Interpret/ptyps.sml")("../Interpret/generate.sml")
13 ("../Interpret/calchead.sml")("../Interpret/appl.sml")
14 ("../Interpret/rewtools.sml")("../Interpret/script.sml")
15 ("../Interpret/solve.sml")("../Interpret/inform.sml")
16 ("../Interpret/mathengine.sml")("../xmlsrc/mathml.sml")
17 ("../xmlsrc/datatypes.sml")("../xmlsrc/pbl-met-hierarchy.sml")
18 ("../xmlsrc/thy-hierarchy.sml")("../xmlsrc/interface-xml.sml")
19 ("../Frontend/messages.sml")("../Frontend/states.sml")
20 ("../Frontend/interface.sml")("../print_exn_G.sml")
24 use "../Interpret/mstools.sml"
25 use "../Interpret/ctree.sml"
26 use "../Interpret/ptyps.sml" (*^^^ need for: fun prep_pbt, fun store_pbt*)
27 use "../Interpret/generate.sml"
28 use "../Interpret/calchead.sml"
29 use "../Interpret/appl.sml"
30 use "../Interpret/rewtools.sml"
31 use "../Interpret/script.sml"
32 use "../Interpret/solve.sml"
33 use "../Interpret/inform.sml" (*^^^ need files for: fun castab*)
34 use "../Interpret/mathengine.sml"
36 use "../xmlsrc/mathml.sml"
37 use "../xmlsrc/datatypes.sml"
38 use "../xmlsrc/pbl-met-hierarchy.sml"
39 use "../xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
40 use "../xmlsrc/interface-xml.sml"
42 use "../Frontend/messages.sml"
43 use "../Frontend/states.sml" (*^^^ need for: val states in Test_Isac.thy*)
44 use "../Frontend/interface.sml"
46 use "../print_exn_G.sml"
54 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
55 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
57 pow :: "[real, real] => real" (infixr "^^^" 80)
58 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
60 (*WN0603 at FE-interface encoded strings to '^',
61 see 'fun encode', fun 'decode'*)
63 abs :: "real => real" ("(|| _ ||)")
64 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
65 absset :: "real set => real" ("(||| _ |||)")
66 (*is numeral constant ?*)
67 is'_const :: "real => bool" ("_ is'_const" 10)
68 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
69 is'_atom :: "real => bool" ("_ is'_atom" 10)
70 is'_even :: "real => bool" ("_ is'_even" 10)
72 (* identity on term level*)
73 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
75 argument'_in :: "real => real" ("argument'_in _" 10)
76 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
77 WN0609 changed the id, because ".. _ _" inhibits currying**)
78 filter'_sameFunId:: "[real, bool list] => bool list"
79 ("filter'_sameFunId _ _" 10)
80 boollist2sum :: "bool list => real"
82 axioms (*for evaluating the assumptions of conditional rules*)
84 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
85 real_unari_minus: "- a = (-1) * a"
87 rle_refl: "(n::real) <= n"
88 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
89 not_true: "(~ True) = False"
90 not_false: "(~ False) = True"
91 and_true: "(a & True) = a"
92 and_false: "(a & False) = False"
93 or_true: "(a | True) = True"
94 or_false: "(a | False) = a"
95 and_commute: "(a & b) = (b & a)"
96 or_commute: "(a | b) = (b | a)"
98 (*.should be in Rational.thy, but:
99 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
100 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
101 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
102 rat_leq2: "d ~= 0 ==>
103 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
104 rat_leq3: "b ~= 0 ==>
105 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
108 text {*copy from doc/math-eng.tex WN.28.3.03
111 section {*Coding standards*}
112 subsection {*Identifiers*}
113 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).
115 This are the preliminary rules for naming identifiers>
117 \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}.
118 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
119 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
120 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
124 %WN071228 extended *}
126 subsection {*Rule sets*}
127 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.
129 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.
132 \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).
134 \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.
136 \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.
137 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).
140 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.
141 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
149 {\tt append_rls, merge_rls, remove_rls} TODO
155 (** evaluation of numerals and special predicates on the meta-level **)
156 (*-------------------------functions---------------------*)
157 local (* rlang 09.02 *)
158 (*.a 'c is coefficient of v' if v does occur in c.*)
159 fun coeff_in v c = member op = (vars c) v;
161 fun occurs_in v t = coeff_in v t;
164 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
165 fun eval_occurs_in _ "Atools.occurs'_in"
166 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
167 ((*tracing("@@@ eval_occurs_in: v= "^(term2str v));
168 tracing("@@@ eval_occurs_in: t= "^(term2str t));*)
170 then SOME ((term2str p) ^ " = True",
171 Trueprop $ (mk_equality (p, HOLogic.true_const)))
172 else SOME ((term2str p) ^ " = False",
173 Trueprop $ (mk_equality (p, HOLogic.false_const))))
174 | eval_occurs_in _ _ _ _ = NONE;
176 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
177 fun some_occur_in vs t =
178 let fun occurs_in' a b = occurs_in b a
179 in foldl or_ (false, map (occurs_in' t) vs) end;
181 (*("some_occur_in", ("Atools.some'_occur'_in",
182 eval_some_occur_in "#eval_some_occur_in_"))*)
183 fun eval_some_occur_in _ "Atools.some'_occur'_in"
184 (p as (Const ("Atools.some'_occur'_in",_)
186 if some_occur_in (isalist2list vs) t
187 then SOME ((term2str p) ^ " = True",
188 Trueprop $ (mk_equality (p, HOLogic.true_const)))
189 else SOME ((term2str p) ^ " = False",
190 Trueprop $ (mk_equality (p, HOLogic.false_const)))
191 | eval_some_occur_in _ _ _ _ = NONE;
196 (*evaluate 'is_atom'*)
197 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
198 fun eval_is_atom (thmid:string) "Atools.is'_atom"
199 (t as (Const(op0,_) $ arg)) thy =
201 Free (n,_) => SOME (mk_thmid thmid op0 n "",
202 Trueprop $ (mk_equality (t, true_as_term)))
203 | _ => SOME (mk_thmid thmid op0 "" "",
204 Trueprop $ (mk_equality (t, false_as_term))))
205 | eval_is_atom _ _ _ _ = NONE;
207 (*evaluate 'is_even'*)
208 fun even i = (i div 2) * 2 = i;
209 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
210 fun eval_is_even (thmid:string) "Atools.is'_even"
211 (t as (Const(op0,_) $ arg)) thy =
214 (case int_of_str n of
216 if even i then SOME (mk_thmid thmid op0 n "",
217 Trueprop $ (mk_equality (t, true_as_term)))
218 else SOME (mk_thmid thmid op0 "" "",
219 Trueprop $ (mk_equality (t, false_as_term)))
222 | eval_is_even _ _ _ _ = NONE;
224 (*evaluate 'is_const'*)
225 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
226 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
227 (t as (Const(op0,t0) $ arg)) (thy:theory) =
228 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
231 SOME (mk_thmid thmid op0 n1 "",
232 Trueprop $ (mk_equality (t, false_as_term)))
235 then SOME (mk_thmid thmid op0 n1 "",
236 Trueprop $ (mk_equality (t, true_as_term)))
237 else SOME (mk_thmid thmid op0 n1 "",
238 Trueprop $ (mk_equality (t, false_as_term)))
239 | Const ("Float.Float",_) =>
240 SOME (mk_thmid thmid op0 (term2str arg) "",
241 Trueprop $ (mk_equality (t, true_as_term)))
243 SOME (mk_thmid thmid op0 (term2str arg) "",
244 Trueprop $ (mk_equality (t, false_as_term))))
245 | eval_const _ _ _ _ = NONE;
247 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
248 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
249 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
250 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
252 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
253 ("xxxxxx",op_,t,thy);
255 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
257 (string_of_int v11)^","^(string_of_int v12)^"), ("^
258 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
259 (string_of_int v21)^","^(string_of_int v22)^"), ("^
260 (string_of_int p21)^","^(string_of_int p22)^"))";
262 (*.convert int and float to internal floatingpoint prepresentation.*)
263 fun numeral (Free (str, T)) =
264 (case int_of_str str of
265 SOME i => SOME ((i, 0), (0, 0))
267 | numeral (Const ("Float.Float", _) $
269 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
270 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
271 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
272 (SOME v1', SOME v2', SOME p1', SOME p2') =>
273 SOME ((v1', v2'), (p1', p2'))
277 (*.evaluate binary associative operations.*)
278 fun eval_binop (thmid:string) (op_:string)
279 (t as ( Const(op0,t0) $
280 (Const(op0',t0') $ v $ t1) $ t2))
281 thy = (*binary . (v.n1).n2*)
283 case (numeral t1, numeral t2) of
284 (SOME n1, SOME n2) =>
285 let val (T1,T2,Trange) = dest_binop_typ t0
286 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
287 (*WN071229 "Rings.inverse_class.divide" never tried*)
288 val rhs = var_op_float v op_ t0 T1 res
289 val prop = Trueprop $ (mk_equality (t, rhs))
290 in SOME (mk_thmid_f thmid n1 n2, prop) end
293 | eval_binop (thmid:string) (op_:string)
295 (Const (op0, t0) $ t1 $
296 (Const (op0', t0') $ t2 $ v)))
297 thy = (*binary . n1.(n2.v)*)
299 case (numeral t1, numeral t2) of
300 (SOME n1, SOME n2) =>
301 if op0 = "Groups.minus_class.minus" then NONE else
302 let val (T1,T2,Trange) = dest_binop_typ t0
303 val res = calc op0 n1 n2
304 val rhs = float_op_var v op_ t0 T1 res
305 val prop = Trueprop $ (mk_equality (t, rhs))
306 in SOME (mk_thmid_f thmid n1 n2, prop) end
310 | eval_binop (thmid:string) (op_:string)
311 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
312 (case (numeral t1, numeral t2) of
313 (SOME n1, SOME n2) =>
314 let val (T1,T2,Trange) = dest_binop_typ t0;
315 val res = calc op0 n1 n2;
316 val rhs = term_of_float Trange res;
317 val prop = Trueprop $ (mk_equality (t, rhs));
318 in SOME (mk_thmid_f thmid n1 n2, prop) end
320 | eval_binop _ _ _ _ = NONE;
322 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
324 val it = "-1 + 2 = 1"
325 > val t = str2term "-1 * (-1 * a)";
326 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
328 val it = "-1 * (-1 * a) = 1 * a"*)
332 (*.evaluate < and <= for numerals.*)
333 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
334 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
335 fun eval_equ (thmid:string) (op_:string) (t as
336 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
337 (case (int_of_str n1, int_of_str n2) of
338 (SOME n1', SOME n2') =>
339 if calc_equ (strip_thy op0) (n1', n2')
340 then SOME (mk_thmid thmid op0 n1 n2,
341 Trueprop $ (mk_equality (t, true_as_term)))
342 else SOME (mk_thmid thmid op0 n1 n2,
343 Trueprop $ (mk_equality (t, false_as_term)))
346 | eval_equ _ _ _ _ = NONE;
351 val it = "(?t = ?t) = True"
352 > val t = str2term "x = 0";
353 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
355 > val t = str2term "1 = 0";
356 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
357 ----------- thus needs Calc !
358 > val t = str2term "0 = 0";
359 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
363 val t = str2term "Not (x = 0)";
370 val it = "x ~= 0" : string*)
372 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
373 the arguments: thus special handling by 'fun eval_binop'*)
374 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
375 fun eval_ident (thmid:string) "Atools.ident" (t as
376 (Const (op0,t0) $ t1 $ t2 )) thy =
378 then SOME (mk_thmid thmid op0
379 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
380 (thy2ctxt thy)) t1) ^ ")")
381 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
382 (thy2ctxt thy)) t2) ^ ")"),
383 Trueprop $ (mk_equality (t, true_as_term)))
384 else SOME (mk_thmid thmid op0
385 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
386 (thy2ctxt thy)) t1) ^ ")")
387 ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
388 (thy2ctxt thy)) t2) ^ ")"),
389 Trueprop $ (mk_equality (t, false_as_term)))
390 | eval_ident _ _ _ _ = NONE;
392 > val t = str2term "x =!= 0";
393 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
395 val str = "ident_(x)_(0)" : string
396 val it = "(x =!= 0) = False" : string
397 > val t = str2term "1 =!= 0";
398 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
400 val str = "ident_(1)_(0)" : string
401 val it = "(1 =!= 0) = False" : string
402 > val t = str2term "0 =!= 0";
403 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
405 val str = "ident_(0)_(0)" : string
406 val it = "(0 =!= 0) = True" : string
409 (*.evaluate identity of terms, which stay ready for evaluation in turn;
410 thus returns False only for atoms.*)
411 (*("equal" ,("op =",eval_equal "#equal_")):calc*)
412 fun eval_equal (thmid : string) "op =" (t as
413 (Const (op0,t0) $ t1 $ t2 )) thy =
415 then SOME (mk_thmid thmid op0
416 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
419 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
422 Trueprop $ (mk_equality (t, true_as_term)))
423 else (case (is_atom t1, is_atom t2) of
425 SOME (mk_thmid thmid op0
426 ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
429 Print_Mode.setmp [] (Syntax.string_of_term
432 Trueprop $ (mk_equality (t, false_as_term)))
433 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
434 | eval_equal _ _ _ _ = NONE; (* error-exit *)
436 val t = str2term "x ~= 0";
437 val NONE = eval_equal "equal_" "b" t thy;
440 > val t = str2term "(x + 1) = (x + 1)";
441 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
443 val str = "equal_(x + 1)_(x + 1)" : string
444 val it = "(x + 1 = x + 1) = True" : string
445 > val t = str2term "x = 0";
446 > val NONE = eval_equal "equal_" "b" t thy;
448 > val t = str2term "1 = 0";
449 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
451 val str = "equal_(1)_(0)" : string
452 val it = "(1 = 0) = False" : string
453 > val t = str2term "0 = 0";
454 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
456 val str = "equal_(0)_(0)" : string
457 val it = "(0 = 0) = True" : string
461 (** evaluation on the metalevel **)
463 (*. evaluate HOL.divide .*)
464 (*("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e"))*)
465 fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as
466 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
467 (case (int_of_str n1, int_of_str n2) of
468 (SOME n1', SOME n2') =>
470 val sg = sign2 n1' n2';
471 val (T1,T2,Trange) = dest_binop_typ t0;
472 val gcd' = gcd (abs n1') (abs n2');
474 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
475 val prop = Trueprop $ (mk_equality (t, rhs))
476 in SOME (mk_thmid thmid op0 n1 n2, prop) end
477 else if 0 < n2' andalso gcd' = 1 then NONE
478 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
480 val prop = Trueprop $ (mk_equality (t, rhs))
481 in SOME (mk_thmid thmid op0 n1 n2, prop) end
483 | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
485 | eval_cancel _ _ _ _ = NONE;
487 (*. get the argument from a function-definition.*)
488 (*("argument_in" ,("Atools.argument'_in",
489 eval_argument_in "Atools.argument'_in"))*)
490 fun eval_argument_in _ "Atools.argument'_in"
491 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
492 if is_Free arg (*could be something to be simplified before*)
493 then SOME (term2str t ^ " = " ^ term2str arg,
494 Trueprop $ (mk_equality (t, arg)))
496 | eval_argument_in _ _ _ _ = NONE;
498 (*.check if the function-identifier of the first argument matches
499 the function-identifier of the lhs of the second argument.*)
500 (*("sameFunId" ,("Atools.sameFunId",
501 eval_same_funid "Atools.sameFunId"))*)
502 fun eval_sameFunId _ "Atools.sameFunId"
503 (p as Const ("Atools.sameFunId",_) $
505 (Const ("op =", _) $ (f2 $ _) $ _)) _ =
507 then SOME ((term2str p) ^ " = True",
508 Trueprop $ (mk_equality (p, HOLogic.true_const)))
509 else SOME ((term2str p) ^ " = False",
510 Trueprop $ (mk_equality (p, HOLogic.false_const)))
511 | eval_sameFunId _ _ _ _ = NONE;
514 (*.from a list of fun-definitions "f x = ..." as 2nd argument
515 filter the elements with the same fun-identfier in "f y"
517 this is, because Isabelles filter takes more than 1 sec.*)
518 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
519 | same_funid f1 t = error ("same_funid called with t = ("
520 ^term2str f1^") ("^term2str t^")");
521 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
522 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
523 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
524 (p as Const ("Atools.filter'_sameFunId",_) $
526 let val fs' = ((list2isalist HOLogic.boolT) o
527 (filter (same_funid fid))) (isalist2list fs)
528 in SOME (term2str (mk_equality (p, fs')),
529 Trueprop $ (mk_equality (p, fs'))) end
530 | eval_filter_sameFunId _ _ _ _ = NONE;
533 (*make a list of terms to a sum*)
534 fun list2sum [] = error ("list2sum called with []")
537 let fun sum su [s'] =
538 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
541 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
545 (*make a list of equalities to the sum of the lhs*)
546 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
547 fun eval_boollist2sum _ "Atools.boollist2sum"
548 (p as Const ("Atools.boollist2sum", _) $
549 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
550 let val isal = isalist2list l
551 val lhss = map lhs isal
552 val sum = list2sum lhss
553 in SOME ((term2str p) ^ " = " ^ (term2str sum),
554 Trueprop $ (mk_equality (p, sum)))
556 | eval_boollist2sum _ _ _ _ = NONE;
565 fun termlessI (_:subst) uv = Term_Ord.termless uv;
566 fun term_ordI (_:subst) uv = Term_Ord.term_ord uv;
570 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
574 append_rls "list_rls" list_rls
575 [Calc ("Groups.times_class.times",eval_binop "#mult_"),
576 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
577 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
578 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
579 Calc ("Atools.ident",eval_ident "#ident_"),
580 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
582 Calc ("Tools.Vars",eval_var "#Vars_"),
584 Thm ("if_True",num_str @{thm if_True}),
585 Thm ("if_False",num_str @{thm if_False})
588 ruleset' := overwritelthy thy (!ruleset',
589 [("list_rls",list_rls)
592 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
593 val tless_true = dummy_ord;
594 rew_ord' := overwritel (!rew_ord',
595 [("tless_true", tless_true),
596 ("e_rew_ord'", tless_true),
597 ("dummy_ord", dummy_ord)]);
599 val calculate_Atools =
600 append_rls "calculate_Atools" e_rls
601 [Calc ("Orderings.ord_class.less",eval_equ "#less_"),
602 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
603 Calc ("op =",eval_equal "#equal_"),
605 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
606 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
607 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
608 Calc ("Groups.times_class.times",eval_binop "#mult_")
612 append_rls "Atools_erls" e_rls
613 [Calc ("op =",eval_equal "#equal_"),
614 Thm ("not_true",num_str @{thm not_true}),
615 (*"(~ True) = False"*)
616 Thm ("not_false",num_str @{thm not_false}),
617 (*"(~ False) = True"*)
618 Thm ("and_true",num_str @{thm and_true}),
619 (*"(?a & True) = ?a"*)
620 Thm ("and_false",num_str @{thm and_false}),
621 (*"(?a & False) = False"*)
622 Thm ("or_true",num_str @{thm or_true}),
623 (*"(?a | True) = True"*)
624 Thm ("or_false",num_str @{thm or_false}),
625 (*"(?a | False) = ?a"*)
627 Thm ("rat_leq1",num_str @{thm rat_leq1}),
628 Thm ("rat_leq2",num_str @{thm rat_leq2}),
629 Thm ("rat_leq3",num_str @{thm rat_leq3}),
630 Thm ("refl",num_str @{thm refl}),
631 Thm ("real_le_refl",num_str @{thm real_le_refl}),
632 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
634 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
635 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
637 Calc ("Atools.ident",eval_ident "#ident_"),
638 Calc ("Atools.is'_const",eval_const "#is_const_"),
639 Calc ("Atools.occurs'_in",eval_occurs_in ""),
640 Calc ("Tools.matches",eval_matches "")
644 append_rls "Atools_crls" e_rls
645 [Calc ("op =",eval_equal "#equal_"),
646 Thm ("not_true",num_str @{thm not_true}),
647 Thm ("not_false",num_str @{thm not_false}),
648 Thm ("and_true",num_str @{thm and_true}),
649 Thm ("and_false",num_str @{thm and_false}),
650 Thm ("or_true",num_str @{thm or_true}),
651 Thm ("or_false",num_str @{thm or_false}),
653 Thm ("rat_leq1",num_str @{thm rat_leq1}),
654 Thm ("rat_leq2",num_str @{thm rat_leq2}),
655 Thm ("rat_leq3",num_str @{thm rat_leq3}),
656 Thm ("refl",num_str @{thm refl}),
657 Thm ("real_le_refl",num_str @{thm real_le_refl}),
658 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
660 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
661 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
663 Calc ("Atools.ident",eval_ident "#ident_"),
664 Calc ("Atools.is'_const",eval_const "#is_const_"),
665 Calc ("Atools.occurs'_in",eval_occurs_in ""),
666 Calc ("Tools.matches",eval_matches "")
669 (*val atools_erls = ... waere zu testen ...
670 merge_rls calculate_Atools
671 (append_rls Atools_erls (*i.A. zu viele rules*)
672 [Calc ("Atools.ident",eval_ident "#ident_"),
673 Calc ("Atools.is'_const",eval_const "#is_const_"),
674 Calc ("Atools.occurs'_in",
675 eval_occurs_in "#occurs_in"),
676 Calc ("Tools.matches",eval_matches "#matches")
677 ] (*i.A. zu viele rules*)
679 (* val atools_erls = prep_rls(
680 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
681 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
682 rules = [Thm ("refl",num_str @{thm refl}),
683 Thm ("real_le_refl",num_str @{thm real_le_refl}),
684 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
685 Thm ("not_true",num_str @{thm not_true}),
686 Thm ("not_false",num_str @{thm not_false}),
687 Thm ("and_true",num_str @{thm and_true}),
688 Thm ("and_false",num_str @{thm and_false}),
689 Thm ("or_true",num_str @{thm or_true}),
690 Thm ("or_false",num_str @{thm or_false}),
691 Thm ("and_commute",num_str @{thm and_commute}),
692 Thm ("or_commute",num_str @{thm or_commute}),
694 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
695 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
697 Calc ("Atools.ident",eval_ident "#ident_"),
698 Calc ("Atools.is'_const",eval_const "#is_const_"),
699 Calc ("Atools.occurs'_in",eval_occurs_in ""),
700 Calc ("Tools.matches",eval_matches "")
702 scr = Script ((term_of o the o (parse @{theory}))
705 ruleset' := overwritelth @{theory}
707 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
710 "******* Atools.ML end *******";
712 calclist':= overwritel (!calclist',
713 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
715 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
716 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
717 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
718 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
719 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
720 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
721 ("ident" ,("Atools.ident",eval_ident "#ident_")),
722 ("equal" ,("op =",eval_equal "#equal_")),
723 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
724 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
725 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
726 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
727 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
728 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
731 val list_rls = prep_rls(
732 merge_rls "list_erls"
733 (Rls {id="replaced",preconds = [],
734 rew_ord = ("termlessI", termlessI),
735 erls = Rls {id="list_elrs", preconds = [],
736 rew_ord = ("termlessI",termlessI),
738 srls = Erls, calc = [], (*asm_thm = [],*)
739 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
740 Calc ("Orderings.ord_class.less",eval_equ "#less_")
741 (* ~~~~~~ for nth_Cons_*)
744 srls = Erls, calc = [], (*asm_thm = [], *)
745 rules = [], scr = EmptyScr})
747 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);