1 (* Title: tools for arithmetic
2 Author: Walther Neuper 010308
3 (c) due to copyright terms
6 theory Atools imports Descript Script
9 subsection \<open>preparation to build up a program from rules\<close>
11 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
12 where "auto_generated t_t = t_t"
13 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
14 where "auto_generated_inst t_t v = t_t"
16 subsection \<open>use preparation\<close>
17 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
19 subsection \<open>consts & axiomatization\<close>
27 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
28 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
30 pow :: "[real, real] => real" (infixr "^^^" 80)
31 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
33 (*WN0603 at FE-interface encoded strings to '^',
34 see 'fun encode', fun 'decode'*)
36 abs :: "real => real" ("(|| _ ||)")
37 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
38 absset :: "real set => real" ("(||| _ |||)")
39 (*is numeral constant ?*)
40 is'_const :: "real => bool" ("_ is'_const" 10)
41 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
42 is'_atom :: "real => bool" ("_ is'_atom" 10)
43 is'_even :: "real => bool" ("_ is'_even" 10)
45 (* identity on term level*)
46 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
48 argument'_in :: "real => real" ("argument'_in _" 10)
49 sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
50 WN0609 changed the id, because ".. _ _" inhibits currying**)
51 filter'_sameFunId:: "[real, bool list] => bool list"
52 ("filter'_sameFunId _ _" 10)
53 boollist2sum :: "bool list => real"
54 lastI :: "'a list \<Rightarrow> 'a"
56 axiomatization where (*for evaluating the assumptions of conditional rules*)
58 last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
59 real_unari_minus: "- a = (-1) * a" and
61 rle_refl: "(n::real) <= n" and
62 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
63 not_true: "(~ True) = False" and
64 not_false: "(~ False) = True"
66 axiomatization where (*..if replaced by "and" we get error:
67 Type unification failed: No type arity bool :: zero ...*)
68 and_true: "(a & True) = a" and
69 and_false: "(a & False) = False" and
70 or_true: "(a | True) = True" and
71 or_false: "(a | False) = a" and
72 and_commute: "(a & b) = (b & a)" and
73 or_commute: "(a | b) = (b | a)"
75 (*.should be in Rational.thy, but:
76 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
77 axiomatization where (*..if replaced by "and" we get error:
78 Type unification failed: No type arity bool :: zero ...*)
79 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
80 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
82 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
84 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
87 subsection \<open>Coding standards\<close>
88 text \<open>copy from doc/math-eng.tex WN.28.3.03
89 WN071228 extended\<close>
91 subsubsection \<open>Identifiers\<close>
92 text \<open>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).
94 This are the preliminary rules for naming identifiers>
96 \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}.
97 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
98 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
99 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
103 %WN071228 extended\<close>
105 subsubsection \<open>Rule sets\<close>
106 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
108 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.
111 \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).
113 \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.
115 \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.
116 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).
119 The above rulesets are all visible to the user, and also may be input;
120 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
121 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
122 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
123 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
131 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
134 subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>
138 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
140 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
141 fun eval_occurs_in _ "Atools.occurs'_in"
142 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
143 ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
144 tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
146 then SOME ((Rule.term2str p) ^ " = True",
147 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
148 else SOME ((Rule.term2str p) ^ " = False",
149 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
150 | eval_occurs_in _ _ _ _ = NONE;
152 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
153 fun some_occur_in vs t =
154 let fun occurs_in' a b = occurs_in b a
155 in foldl or_ (false, map (occurs_in' t) vs) end;
157 (*("some_occur_in", ("Atools.some'_occur'_in",
158 eval_some_occur_in "#eval_some_occur_in_"))*)
159 fun eval_some_occur_in _ "Atools.some'_occur'_in"
160 (p as (Const ("Atools.some'_occur'_in",_)
162 if some_occur_in (TermC.isalist2list vs) t
163 then SOME ((Rule.term2str p) ^ " = True",
164 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
165 else SOME ((Rule.term2str p) ^ " = False",
166 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
167 | eval_some_occur_in _ _ _ _ = NONE;
172 (*evaluate 'is_atom'*)
173 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
174 fun eval_is_atom (thmid:string) "Atools.is'_atom"
175 (t as (Const(op0,_) $ arg)) thy =
177 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
178 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
179 | _ => SOME (TermC.mk_thmid thmid "" "",
180 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
181 | eval_is_atom _ _ _ _ = NONE;
183 (*evaluate 'is_even'*)
184 fun even i = (i div 2) * 2 = i;
185 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
186 fun eval_is_even (thmid:string) "Atools.is'_even"
187 (t as (Const(op0,_) $ arg)) thy =
190 (case TermC.int_of_str_opt n of
192 if even i then SOME (TermC.mk_thmid thmid n "",
193 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
194 else SOME (TermC.mk_thmid thmid "" "",
195 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
198 | eval_is_even _ _ _ _ = NONE;
200 (*evaluate 'is_const'*)
201 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
202 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
203 (t as (Const(op0,t0) $ arg)) (thy:theory) =
204 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
207 SOME (TermC.mk_thmid thmid n1 "",
208 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
211 then SOME (TermC.mk_thmid thmid n1 "",
212 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
213 else SOME (TermC.mk_thmid thmid n1 "",
214 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
215 | Const ("Float.Float",_) =>
216 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
217 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
219 SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
220 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
221 | eval_const _ _ _ _ = NONE;
223 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
224 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
225 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
226 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
228 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
229 ("xxxxxx",op_,t,thy);
231 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
233 (string_of_int v11)^","^(string_of_int v12)^"), ("^
234 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
235 (string_of_int v21)^","^(string_of_int v22)^"), ("^
236 (string_of_int p21)^","^(string_of_int p22)^"))";
238 (*.convert int and float to internal floatingpoint prepresentation.*)
239 fun numeral (Free (str, T)) =
240 (case TermC.int_of_str_opt str of
241 SOME i => SOME ((i, 0), (0, 0))
243 | numeral (Const ("Float.Float", _) $
244 (Const ("Product_Type.Pair", _) $
245 (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
246 (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
247 (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
248 (SOME v1', SOME v2', SOME p1', SOME p2') =>
249 SOME ((v1', v2'), (p1', p2'))
253 (* evaluate binary associative operations *)
254 fun eval_binop (thmid : string) (op_: string)
255 (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
257 case (numeral t1, numeral t2) of
258 (SOME n1, SOME n2) =>
260 val (T1, _, _) = TermC.dest_binop_typ t0
262 calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
263 (*WN071229 "Rings.divide_class.divide" never tried*)
264 val rhs = var_op_float v op_ t0 T1 res
265 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
266 in SOME ("#: " ^ Rule.term2str prop, prop) end
269 | eval_binop (thmid : string) (op_ : string)
270 (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
272 case (numeral t1, numeral t2) of
273 (SOME n1, SOME n2) =>
274 if op0 = "Groups.minus_class.minus" then NONE
276 val (T1, _, _) = TermC.dest_binop_typ t0
277 val res = calcul op0 n1 n2
278 val rhs = float_op_var v op_ t0 T1 res
279 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
280 in SOME ("#: " ^ Rule.term2str prop, prop) end
283 | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
284 (case (numeral t1, numeral t2) of
285 (SOME n1, SOME n2) =>
287 val (_, _, Trange) = TermC.dest_binop_typ t0;
288 val res = calcul op0 n1 n2;
289 val rhs = term_of_float Trange res;
290 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
291 in SOME ("#: " ^ Rule.term2str prop, prop) end
293 | eval_binop _ _ _ _ = NONE;
295 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
297 val it = "-1 + 2 = 1"
298 > val t = str2term "-1 * (-1 * a)";
299 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
301 val it = "-1 * (-1 * a) = 1 * a"*)
305 (*.evaluate < and <= for numerals.*)
306 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
307 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
308 fun eval_equ (thmid:string) (op_:string) (t as
309 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
310 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
311 (SOME n1', SOME n2') =>
312 if Calc.calc_equ (strip_thy op0) (n1', n2')
313 then SOME (TermC.mk_thmid thmid n1 n2,
314 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
315 else SOME (TermC.mk_thmid thmid n1 n2,
316 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
319 | eval_equ _ _ _ _ = NONE;
324 val it = "(?t = ?t) = True"
325 > val t = str2term "x = 0";
326 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
328 > val t = str2term "1 = 0";
329 > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
330 ----------- thus needs Rule.Calc !
331 > val t = str2term "0 = 0";
332 > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
336 val t = str2term "Not (x = 0)";
337 atomt t; Rule.term2str t;
343 val it = "x ~= 0" : string*)
345 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
346 the arguments: thus special handling by 'fun eval_binop'*)
347 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
348 fun eval_ident (thmid:string) "Atools.ident" (t as
349 (Const (op0,t0) $ t1 $ t2 )) thy =
351 then SOME (TermC.mk_thmid thmid
352 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
353 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
354 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
355 else SOME (TermC.mk_thmid thmid
356 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
357 ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
358 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
359 | eval_ident _ _ _ _ = NONE;
361 > val t = str2term "x =!= 0";
362 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
364 val str = "ident_(x)_(0)" : string
365 val it = "(x =!= 0) = False" : string
366 > val t = str2term "1 =!= 0";
367 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
369 val str = "ident_(1)_(0)" : string
370 val it = "(1 =!= 0) = False" : string
371 > val t = str2term "0 =!= 0";
372 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
374 val str = "ident_(0)_(0)" : string
375 val it = "(0 =!= 0) = True" : string
378 (*.evaluate identity of terms, which stay ready for evaluation in turn;
379 thus returns False only for atoms.*)
380 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
381 fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy =
383 then SOME (TermC.mk_thmid thmid
384 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
385 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
386 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
387 else (case (TermC.is_atom t1, TermC.is_atom t2) of
389 SOME (TermC.mk_thmid thmid
390 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
391 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
392 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
393 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
394 | eval_equal _ _ _ _ = NONE; (* error-exit *)
396 val t = str2term "x ~= 0";
397 val NONE = eval_equal "equal_" "b" t thy;
400 > val t = str2term "(x + 1) = (x + 1)";
401 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
403 val str = "equal_(x + 1)_(x + 1)" : string
404 val it = "(x + 1 = x + 1) = True" : string
405 > val t = str2term "x = 0";
406 > val NONE = eval_equal "equal_" "b" t thy;
408 > val t = str2term "1 = 0";
409 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
411 val str = "equal_(1)_(0)" : string
412 val it = "(1 = 0) = False" : string
413 > val t = str2term "0 = 0";
414 > val SOME (str, t') = eval_equal "equal_" "b" t thy;
416 val str = "equal_(0)_(0)" : string
417 val it = "(0 = 0) = True" : string
423 subsection \<open>evaluation on the meta-level\<close>
425 (*. evaluate HOL.divide .*)
426 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
427 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
428 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
429 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
430 (SOME n1', SOME n2') =>
432 val sg = Calc.sign_mult n1' n2';
433 val (T1,T2,Trange) = TermC.dest_binop_typ t0;
434 val gcd' = Calc.gcd (abs n1') (abs n2');
436 then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
437 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
438 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
439 else if 0 < n2' andalso gcd' = 1 then NONE
440 else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
442 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
443 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
445 | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
447 | eval_cancel _ _ _ _ = NONE;
449 (*. get the argument from a function-definition.*)
450 (*("argument_in" ,("Atools.argument'_in",
451 eval_argument_in "Atools.argument'_in"))*)
452 fun eval_argument_in _ "Atools.argument'_in"
453 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
454 if is_Free arg (*could be something to be simplified before*)
455 then SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
456 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
458 | eval_argument_in _ _ _ _ = NONE;
460 (*.check if the function-identifier of the first argument matches
461 the function-identifier of the lhs of the second argument.*)
462 (*("sameFunId" ,("Atools.sameFunId",
463 eval_same_funid "Atools.sameFunId"))*)
464 fun eval_sameFunId _ "Atools.sameFunId"
465 (p as Const ("Atools.sameFunId",_) $
467 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
469 then SOME ((Rule.term2str p) ^ " = True",
470 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
471 else SOME ((Rule.term2str p) ^ " = False",
472 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
473 | eval_sameFunId _ _ _ _ = NONE;
476 (*.from a list of fun-definitions "f x = ..." as 2nd argument
477 filter the elements with the same fun-identfier in "f y"
479 this is, because Isabelles filter takes more than 1 sec.*)
480 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
481 | same_funid f1 t = error ("same_funid called with t = ("
482 ^Rule.term2str f1^") ("^Rule.term2str t^")");
483 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
484 eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
485 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
486 (p as Const ("Atools.filter'_sameFunId",_) $
488 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
489 (filter (same_funid fid))) (TermC.isalist2list fs)
490 in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
491 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
492 | eval_filter_sameFunId _ _ _ _ = NONE;
495 (*make a list of terms to a sum*)
496 fun list2sum [] = error ("list2sum called with []")
499 let fun sum su [s'] =
500 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
503 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
507 (*make a list of equalities to the sum of the lhs*)
508 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
509 fun eval_boollist2sum _ "Atools.boollist2sum"
510 (p as Const ("Atools.boollist2sum", _) $
511 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
512 let val isal = TermC.isalist2list l
513 val lhss = map Tools.lhs isal
514 val sum = list2sum lhss
515 in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
516 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
518 | eval_boollist2sum _ _ _ _ = NONE;
521 subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>
528 fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
529 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
532 val list_rls = Rule.append_rls "list_rls" list_rls
533 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
534 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
535 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
536 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
537 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
538 Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
540 Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
542 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
543 Rule.Thm ("if_False",TermC.num_str @{thm if_False})
548 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
549 val tless_true = Rule.dummy_ord;
550 Rule.rew_ord' := overwritel (! Rule.rew_ord',
551 [("tless_true", tless_true),
552 ("e_rew_ord'", tless_true),
553 ("dummy_ord", Rule.dummy_ord)]);
555 val calculate_Base_Tools =
556 Rule.append_rls "calculate_Atools" Rule.e_rls
557 [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
558 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
559 Rule.Calc ("HOL.eq",eval_equal "#equal_"),
561 Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
562 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
563 Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
564 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_")
569 find_theorems (9) "?n <= ?n"
573 Rule.append_rls "Atools_erls" Rule.e_rls
574 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
575 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
576 (*"(~ True) = False"*)
577 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
578 (*"(~ False) = True"*)
579 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
580 (*"(?a & True) = ?a"*)
581 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
582 (*"(?a & False) = False"*)
583 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
584 (*"(?a | True) = True"*)
585 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
586 (*"(?a | False) = ?a"*)
588 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
589 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
590 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
591 Rule.Thm ("refl",TermC.num_str @{thm refl}),
592 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
593 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
595 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
596 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
598 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
599 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
600 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
601 Rule.Calc ("Tools.matches", Tools.eval_matches "")
608 Rule.append_rls "Atools_crls" Rule.e_rls
609 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
610 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
611 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
612 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
613 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
614 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
615 Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
617 Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
618 Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
619 Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
620 Rule.Thm ("refl",TermC.num_str @{thm refl}),
621 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
622 Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
624 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
625 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
627 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
628 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
629 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
630 Rule.Calc ("Tools.matches", Tools.eval_matches "")
633 (*val atools_erls = ... waere zu testen ...
634 Rule.merge_rls calculate_Atools
635 (Rule.append_rls Atools_erls (*i.A. zu viele rules*)
636 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
637 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
638 Rule.Calc ("Atools.occurs'_in",
639 eval_occurs_in "#occurs_in"),
640 Rule.Calc ("Tools.matches",eval_matches "#matches")
641 ] (*i.A. zu viele rules*)
643 (* val atools_erls = prep_rls'( (*outcommented*)
644 Rule.Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
645 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
646 rules = [Rule.Thm ("refl",num_str @{thm refl}),
647 Rule.Thm ("order_refl",num_str @{thm order_refl}),
648 Rule.Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
649 Rule.Thm ("not_true",num_str @{thm not_true}),
650 Rule.Thm ("not_false",num_str @{thm not_false}),
651 Rule.Thm ("and_true",num_str @{thm and_true}),
652 Rule.Thm ("and_false",num_str @{thm and_false}),
653 Rule.Thm ("or_true",num_str @{thm or_true}),
654 Rule.Thm ("or_false",num_str @{thm or_false}),
655 Rule.Thm ("and_commute",num_str @{thm and_commute}),
656 Rule.Thm ("or_commute",num_str @{thm or_commute}),
658 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
659 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
661 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
662 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
663 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
664 Rule.Calc ("Tools.matches",eval_matches "")
666 scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
669 "******* Atools.ML end *******";
671 subsection \<open>write to KEStore: calcs, rule-sets\<close>
672 setup \<open>KEStore_Elems.add_calcs
673 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
675 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
676 ("is_atom" ,("Atools.is'_atom", eval_is_atom "#is_atom_")),
677 ("is_even" ,("Atools.is'_even", eval_is_even "#is_even_")),
678 ("is_const" ,("Atools.is'_const", eval_const "#is_const_")),
679 ("le" ,("Orderings.ord_class.less", eval_equ "#less_")),
680 ("leq" ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
681 ("ident" ,("Atools.ident", eval_ident "#ident_")),
682 ("equal" ,("HOL.eq", eval_equal "#equal_")),
683 ("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
684 ("MINUS" ,("Groups.minus_class.minus", eval_binop "#sub_")),
685 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
686 ("DIVIDE" ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
687 ("POWER" ,("Atools.pow", eval_binop "#power_")),
688 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
690 val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
691 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
692 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
693 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
694 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
695 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
696 (* ~~~~~~ for nth_Cons_*)],
697 scr = Rule.EmptyScr},
698 srls = Rule.Erls, calc = [], errpatts = [],
699 rules = [], scr = Rule.EmptyScr})
702 setup \<open>KEStore_Elems.add_rlss
703 [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>