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"
45 axiomatization where (*for evaluating the assumptions of conditional rules*)
47 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
48 real_unari_minus: "- a = (-1) * a" and
50 rle_refl: "(n::real) <= n" and
51 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
52 not_true: "(~ True) = False" and
53 not_false: "(~ False) = True"
55 axiomatization where (*..if replaced by "and" we get error:
56 Type unification failed: No type arity bool :: zero ...*)
57 and_true: "(a & True) = a" and
58 and_false: "(a & False) = False" and
59 or_true: "(a | True) = True" and
60 or_false: "(a | False) = a" and
61 and_commute: "(a & b) = (b & a)" and
62 or_commute: "(a | b) = (b | a)"
64 (*.should be in Rational.thy, but:
65 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
66 axiomatization where (*..if replaced by "and" we get error:
67 Type unification failed: No type arity bool :: zero ...*)
68 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
69 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
71 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
73 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
76 text {*copy from doc/math-eng.tex WN.28.3.03
79 section {*Coding standards*}
80 subsection {*Identifiers*}
81 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).
83 This are the preliminary rules for naming identifiers>
85 \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}.
86 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
87 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
88 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
94 subsection {*Rule sets*}
95 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.
97 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.
100 \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).
102 \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.
104 \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.
105 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).
108 The above rulesets are all visible to the user, and also may be input;
109 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
110 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
111 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
112 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
120 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
126 (** evaluation of numerals and special predicates on the meta-level **)
127 (*-------------------------functions---------------------*)
128 local (* rlang 09.02 *)
129 (*.a 'c is coefficient of v' if v does occur in c.*)
130 fun coeff_in v c = member op = (TermC.vars c) v;
132 fun occurs_in v t = coeff_in v t;
135 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
136 fun eval_occurs_in _ "Atools.occurs'_in"
137 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
138 ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
139 tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
141 then SOME ((Rule.term2str p) ^ " = True",
142 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
143 else SOME ((Rule.term2str p) ^ " = False",
144 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
145 | eval_occurs_in _ _ _ _ = NONE;
147 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
148 fun some_occur_in vs t =
149 let fun occurs_in' a b = occurs_in b a
150 in foldl or_ (false, map (occurs_in' t) vs) end;
152 (*("some_occur_in", ("Atools.some'_occur'_in",
153 eval_some_occur_in "#eval_some_occur_in_"))*)
154 fun eval_some_occur_in _ "Atools.some'_occur'_in"
155 (p as (Const ("Atools.some'_occur'_in",_)
157 if some_occur_in (TermC.isalist2list vs) t
158 then SOME ((Rule.term2str p) ^ " = True",
159 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
160 else SOME ((Rule.term2str p) ^ " = False",
161 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
162 | eval_some_occur_in _ _ _ _ = NONE;
167 (*evaluate 'is_atom'*)
168 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
169 fun eval_is_atom (thmid:string) "Atools.is'_atom"
170 (t as (Const(op0,_) $ arg)) thy =
172 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
173 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
174 | _ => SOME (TermC.mk_thmid thmid "" "",
175 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
176 | eval_is_atom _ _ _ _ = NONE;
178 (*evaluate 'is_even'*)
179 fun even i = (i div 2) * 2 = i;
180 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
181 fun eval_is_even (thmid:string) "Atools.is'_even"
182 (t as (Const(op0,_) $ arg)) thy =
185 (case TermC.int_of_str_opt n of
187 if even i then SOME (TermC.mk_thmid thmid n "",
188 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
189 else SOME (TermC.mk_thmid thmid "" "",
190 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
193 | eval_is_even _ _ _ _ = NONE;
195 (*evaluate 'is_const'*)
196 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
197 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
198 (t as (Const(op0,t0) $ arg)) (thy:theory) =
199 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
202 SOME (TermC.mk_thmid thmid n1 "",
203 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
206 then SOME (TermC.mk_thmid thmid n1 "",
207 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
208 else SOME (TermC.mk_thmid thmid n1 "",
209 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
210 | Const ("Float.Float",_) =>
211 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
212 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
214 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
215 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
216 | eval_const _ _ _ _ = NONE;
218 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
219 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
220 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
221 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
223 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
224 ("xxxxxx",op_,t,thy);
226 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
228 (string_of_int v11)^","^(string_of_int v12)^"), ("^
229 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
230 (string_of_int v21)^","^(string_of_int v22)^"), ("^
231 (string_of_int p21)^","^(string_of_int p22)^"))";
233 (*.convert int and float to internal floatingpoint prepresentation.*)
234 fun numeral (Free (str, T)) =
235 (case TermC.int_of_str_opt str of
236 SOME i => SOME ((i, 0), (0, 0))
238 | numeral (Const ("Float.Float", _) $
239 (Const ("Product_Type.Pair", _) $
240 (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
241 (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
242 (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
243 (SOME v1', SOME v2', SOME p1', SOME p2') =>
244 SOME ((v1', v2'), (p1', p2'))
248 (* evaluate binary associative operations *)
249 fun eval_binop (thmid : string) (op_: string)
250 (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
252 case (numeral t1, numeral t2) of
253 (SOME n1, SOME n2) =>
255 val (T1, _, _) = TermC.dest_binop_typ t0
257 calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
258 (*WN071229 "Rings.divide_class.divide" never tried*)
259 val rhs = var_op_float v op_ t0 T1 res
260 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
261 in SOME ("#: " ^ Rule.term2str prop, prop) end
264 | eval_binop (thmid : string) (op_ : string)
265 (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
267 case (numeral t1, numeral t2) of
268 (SOME n1, SOME n2) =>
269 if op0 = "Groups.minus_class.minus" then NONE
271 val (T1, _, _) = TermC.dest_binop_typ t0
272 val res = calcul op0 n1 n2
273 val rhs = float_op_var v op_ t0 T1 res
274 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
275 in SOME ("#: " ^ Rule.term2str prop, prop) end
278 | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
279 (case (numeral t1, numeral t2) of
280 (SOME n1, SOME n2) =>
282 val (_, _, Trange) = TermC.dest_binop_typ t0;
283 val res = calcul op0 n1 n2;
284 val rhs = term_of_float Trange res;
285 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
286 in SOME ("#: " ^ Rule.term2str prop, prop) end
288 | eval_binop _ _ _ _ = NONE;
290 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
292 val it = "-1 + 2 = 1"
293 > val t = str2term "-1 * (-1 * a)";
294 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
296 val it = "-1 * (-1 * a) = 1 * a"*)
300 (*.evaluate < and <= for numerals.*)
301 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
302 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
303 fun eval_equ (thmid:string) (op_:string) (t as
304 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
305 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
306 (SOME n1', SOME n2') =>
307 if Calc.calc_equ (strip_thy op0) (n1', n2')
308 then SOME (TermC.mk_thmid thmid n1 n2,
309 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
310 else SOME (TermC.mk_thmid thmid n1 n2,
311 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
314 | eval_equ _ _ _ _ = NONE;
319 val it = "(?t = ?t) = True"
320 > val t = str2term "x = 0";
321 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
323 > val t = str2term "1 = 0";
324 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
325 ----------- thus needs Rule.Calc !
326 > val t = str2term "0 = 0";
327 > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
331 val t = str2term "Not (x = 0)";
332 atomt t; Rule.term2str t;
338 val it = "x ~= 0" : string*)
340 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
341 the arguments: thus special handling by 'fun eval_binop'*)
342 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
343 fun eval_ident (thmid:string) "Atools.ident" (t as
344 (Const (op0,t0) $ t1 $ t2 )) thy =
346 then SOME (TermC.mk_thmid thmid
347 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
348 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
349 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
350 else SOME (TermC.mk_thmid thmid
351 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
352 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
353 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
354 | eval_ident _ _ _ _ = NONE;
356 > val t = str2term "x =!= 0";
357 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
359 val str = "ident_(x)_(0)" : string
360 val it = "(x =!= 0) = False" : string
361 > val t = str2term "1 =!= 0";
362 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
364 val str = "ident_(1)_(0)" : string
365 val it = "(1 =!= 0) = False" : string
366 > val t = str2term "0 =!= 0";
367 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
369 val str = "ident_(0)_(0)" : string
370 val it = "(0 =!= 0) = True" : string
373 (*.evaluate identity of terms, which stay ready for evaluation in turn;
374 thus returns False only for atoms.*)
375 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
376 fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy =
378 then SOME (TermC.mk_thmid thmid
379 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
380 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
381 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
382 else (case (TermC.is_atom t1, TermC.is_atom t2) of
384 SOME (TermC.mk_thmid thmid
385 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
386 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
387 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
388 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
389 | eval_equal _ _ _ _ = NONE; (* error-exit *)
391 val t = str2term "x ~= 0";
392 val NONE = eval_equal "equal_" "b" t thy;
395 > val t = str2term "(x + 1) = (x + 1)";
396 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
398 val str = "equal_(x + 1)_(x + 1)" : string
399 val it = "(x + 1 = x + 1) = True" : string
400 > val t = str2term "x = 0";
401 > val NONE = eval_equal "equal_" "b" t thy;
403 > val t = str2term "1 = 0";
404 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
406 val str = "equal_(1)_(0)" : string
407 val it = "(1 = 0) = False" : string
408 > val t = str2term "0 = 0";
409 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
411 val str = "equal_(0)_(0)" : string
412 val it = "(0 = 0) = True" : string
419 (** evaluation on the metalevel **)
421 (*. evaluate HOL.divide .*)
422 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
423 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
424 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
425 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
426 (SOME n1', SOME n2') =>
428 val sg = Calc.sign_mult n1' n2';
429 val (T1,T2,Trange) = TermC.dest_binop_typ t0;
430 val gcd' = Calc.gcd (abs n1') (abs n2');
432 then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
433 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
434 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
435 else if 0 < n2' andalso gcd' = 1 then NONE
436 else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
438 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
439 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
441 | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
443 | eval_cancel _ _ _ _ = NONE;
445 (*. get the argument from a function-definition.*)
446 (*("argument_in" ,("Atools.argument'_in",
447 eval_argument_in "Atools.argument'_in"))*)
448 fun eval_argument_in _ "Atools.argument'_in"
449 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
450 if is_Free arg (*could be something to be simplified before*)
451 then SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
452 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
454 | eval_argument_in _ _ _ _ = NONE;
456 (*.check if the function-identifier of the first argument matches
457 the function-identifier of the lhs of the second argument.*)
458 (*("sameFunId" ,("Atools.sameFunId",
459 eval_same_funid "Atools.sameFunId"))*)
460 fun eval_sameFunId _ "Atools.sameFunId"
461 (p as Const ("Atools.sameFunId",_) $
463 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
465 then SOME ((Rule.term2str p) ^ " = True",
466 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
467 else SOME ((Rule.term2str p) ^ " = False",
468 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
469 | eval_sameFunId _ _ _ _ = NONE;
472 (*.from a list of fun-definitions "f x = ..." as 2nd argument
473 filter the elements with the same fun-identfier in "f y"
475 this is, because Isabelles filter takes more than 1 sec.*)
476 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
477 | same_funid f1 t = error ("same_funid called with t = ("
478 ^Rule.term2str f1^") ("^Rule.term2str t^")");
479 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
480 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
481 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
482 (p as Const ("Atools.filter'_sameFunId",_) $
484 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
485 (filter (same_funid fid))) (TermC.isalist2list fs)
486 in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
487 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
488 | eval_filter_sameFunId _ _ _ _ = NONE;
491 (*make a list of terms to a sum*)
492 fun list2sum [] = error ("list2sum called with []")
495 let fun sum su [s'] =
496 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
499 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
503 (*make a list of equalities to the sum of the lhs*)
504 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
505 fun eval_boollist2sum _ "Atools.boollist2sum"
506 (p as Const ("Atools.boollist2sum", _) $
507 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
508 let val isal = TermC.isalist2list l
509 val lhss = map lhs isal
510 val sum = list2sum lhss
511 in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
512 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
514 | eval_boollist2sum _ _ _ _ = NONE;
523 fun termlessI (_: Rule.subst) uv = Term_Ord.termless uv;
524 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
528 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
531 val list_rls = Rule.append_rls "list_rls" list_rls
532 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
533 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
534 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
535 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
536 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
537 Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
539 Rule.Calc ("Tools.Vars",eval_var "#Vars_"),
541 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
542 Rule.Thm ("if_False",TermC.num_str @{thm if_False})
547 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
548 val tless_true = Rule.dummy_ord;
549 Rule.rew_ord' := overwritel (! Rule.rew_ord',
550 [("tless_true", tless_true),
551 ("e_rew_ord'", tless_true),
552 ("dummy_ord", Rule.dummy_ord)]);
554 val calculate_Base_Tools =
555 Rule.append_rls "calculate_Atools" Rule.e_rls
556 [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
557 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
558 Rule.Calc ("HOL.eq",eval_equal "#equal_"),
560 Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
561 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
562 Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
563 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_")
568 find_theorems (9) "?n <= ?n"
572 Rule.append_rls "Atools_erls" Rule.e_rls
573 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
574 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
575 (*"(~ True) = False"*)
576 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
577 (*"(~ False) = True"*)
578 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
579 (*"(?a & True) = ?a"*)
580 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
581 (*"(?a & False) = False"*)
582 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
583 (*"(?a | True) = True"*)
584 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
585 (*"(?a | False) = ?a"*)
587 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
588 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
589 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
590 Rule.Thm ("refl",TermC.num_str @{thm refl}),
591 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
592 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
594 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
595 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
597 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
598 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
599 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
600 Rule.Calc ("Tools.matches",eval_matches "")
607 Rule.append_rls "Atools_crls" Rule.e_rls
608 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
609 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
610 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
611 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
612 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
613 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
614 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
616 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
617 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
618 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
619 Rule.Thm ("refl",TermC.num_str @{thm refl}),
620 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
621 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
623 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
624 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
626 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
627 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
628 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
629 Rule.Calc ("Tools.matches",eval_matches "")
632 (*val atools_erls = ... waere zu testen ...
633 Rule.merge_rls calculate_Atools
634 (Rule.append_rls Atools_erls (*i.A. zu viele rules*)
635 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
636 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
637 Rule.Calc ("Atools.occurs'_in",
638 eval_occurs_in "#occurs_in"),
639 Rule.Calc ("Tools.matches",eval_matches "#matches")
640 ] (*i.A. zu viele rules*)
642 (* val atools_erls = prep_rls'( (*outcommented*)
643 Rule.Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
644 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
645 rules = [Rule.Thm ("refl",num_str @{thm refl}),
646 Rule.Thm ("order_refl",num_str @{thm order_refl}),
647 Rule.Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
648 Rule.Thm ("not_true",num_str @{thm not_true}),
649 Rule.Thm ("not_false",num_str @{thm not_false}),
650 Rule.Thm ("and_true",num_str @{thm and_true}),
651 Rule.Thm ("and_false",num_str @{thm and_false}),
652 Rule.Thm ("or_true",num_str @{thm or_true}),
653 Rule.Thm ("or_false",num_str @{thm or_false}),
654 Rule.Thm ("and_commute",num_str @{thm and_commute}),
655 Rule.Thm ("or_commute",num_str @{thm or_commute}),
657 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
658 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
660 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
661 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
662 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
663 Rule.Calc ("Tools.matches",eval_matches "")
665 scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
668 "******* Atools.ML end *******";
670 setup {* KEStore_Elems.add_calcs
671 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
673 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
674 ("is_atom" ,("Atools.is'_atom", eval_is_atom "#is_atom_")),
675 ("is_even" ,("Atools.is'_even", eval_is_even "#is_even_")),
676 ("is_const" ,("Atools.is'_const", eval_const "#is_const_")),
677 ("le" ,("Orderings.ord_class.less", eval_equ "#less_")),
678 ("leq" ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
679 ("ident" ,("Atools.ident", eval_ident "#ident_")),
680 ("equal" ,("HOL.eq", eval_equal "#equal_")),
681 ("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
682 ("MINUS" ,("Groups.minus_class.minus", eval_binop "#sub_")),
683 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
684 ("DIVIDE" ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
685 ("POWER" ,("Atools.pow", eval_binop "#power_")),
686 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
688 val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
689 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
690 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
691 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
692 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
693 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
694 (* ~~~~~~ for nth_Cons_*)],
695 scr = Rule.EmptyScr},
696 srls = Rule.Erls, calc = [], errpatts = [],
697 rules = [], scr = Rule.EmptyScr})
700 setup {* KEStore_Elems.add_rlss
701 [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))] *}