neuper@37944: (* Title:  tools for arithmetic
neuper@37944:    Author: Walther Neuper 010308
neuper@37944:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
wneuper@59424: theory Atools imports Descript Script
neuper@37967: begin
neuper@37906: 
wneuper@59424: ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
wneuper@59424: 
neuper@37906: consts
neuper@37906: 
neuper@37946:   Arbfix           :: "real"
neuper@37949:   Undef            :: "real"
neuper@37949:   dummy            :: "real"
neuper@37949: 
neuper@37949:   some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
neuper@37949:   occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
neuper@37949: 
neuper@37949:   pow              :: "[real, real] => real"    (infixr "^^^" 80)
neuper@37949: (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
neuper@37949:                            ~~~~     ~~~~    ~~~~     ~~~*)
neuper@37949: (*WN0603 at FE-interface encoded strings to '^', 
neuper@37949: 	see 'fun encode', fun 'decode'*)
neuper@37949: 
neuper@37949:   abs              :: "real => real"            ("(|| _ ||)")
neuper@37949: (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
neuper@37949:   absset           :: "real set => real"        ("(||| _ |||)")
neuper@37949:   (*is numeral constant ?*)
neuper@37949:   is'_const        :: "real => bool"            ("_ is'_const" 10)
neuper@37949:   (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
neuper@37949:   is'_atom         :: "real => bool"            ("_ is'_atom" 10)
neuper@37949:   is'_even         :: "real => bool"            ("_ is'_even" 10)
neuper@37949: 		
neuper@37949:   (* identity on term level*)
neuper@37949:   ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)
neuper@37949: 
neuper@37949:   argument'_in     :: "real => real"            ("argument'_in _" 10)
neuper@37949:   sameFunId        :: "[real, bool] => bool"    (**"same'_funid _ _" 10
neuper@37949: 	WN0609 changed the id, because ".. _ _" inhibits currying**)
neuper@37949:   filter'_sameFunId:: "[real, bool list] => bool list" 
neuper@37949: 					        ("filter'_sameFunId _ _" 10)
neuper@37949:   boollist2sum     :: "bool list => real"
wneuper@59429:   lastI            :: "'a list \<Rightarrow> 'a"
neuper@37949: 
neuper@52148: axiomatization where (*for evaluating the assumptions of conditional rules*)
neuper@37949: 
neuper@52148:   last_thmI:	      "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
neuper@52148:   real_unari_minus:   "- a = (-1) * a" and
neuper@37949: 
neuper@52148:   rle_refl:           "(n::real) <= n" and
neuper@52148:   radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
neuper@52148:   not_true:           "(~ True) = False" and
neuper@37965:   not_false:          "(~ False) = True"
neuper@52148: 
neuper@52148: axiomatization where (*..if replaced by "and" we get error:
t@42203: Type unification failed: No type arity bool :: zero ...*)
neuper@52148:   and_true:           "(a & True) = a" and
neuper@52148:   and_false:          "(a & False) = False" and
neuper@52148:   or_true:            "(a | True) = True" and
neuper@52148:   or_false:           "(a | False) = a" and
neuper@52148:   and_commute:        "(a & b) = (b & a)" and
t@42203:   or_commute:         "(a | b) = (b | a)" 
neuper@37949: 
neuper@37949:   (*.should be in Rational.thy, but: 
neuper@37949:    needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
neuper@52148: axiomatization where (*..if replaced by "and" we get error:
t@42203: Type unification failed: No type arity bool :: zero ...*)
neuper@37965:   rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
neuper@52148: 		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
neuper@37965:   rat_leq2:	      "d ~= 0 ==>
neuper@52148: 		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
neuper@37965:   rat_leq3:	      "b ~= 0 ==>
neuper@37949: 		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
neuper@37949: 
neuper@37965: 
neuper@37949: text {*copy from doc/math-eng.tex WN.28.3.03
neuper@37949: WN071228 extended *}
neuper@37949: 
neuper@37949: section {*Coding standards*}
neuper@37949: subsection {*Identifiers*}
neuper@37949: 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).
neuper@37949: 
neuper@37949: This are the preliminary rules for naming identifiers>
neuper@37949: \begin{description}
neuper@37949: \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}.
neuper@37949: \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
neuper@37949: \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
neuper@37949: \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
neuper@37949: \item [???] ???
neuper@37949: \item [???] ???
neuper@37949: \end{description}
neuper@37949: %WN071228 extended *}
neuper@37949: 
neuper@37949: subsection {*Rule sets*}
neuper@37949: 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.
neuper@37949: 
neuper@37949: 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.
neuper@37949: \begin{description}
neuper@37949: 
neuper@37949: \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).
neuper@37949: 
neuper@37949: \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.
neuper@37949: 
neuper@37949: \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.
neuper@37949: 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).
neuper@37949: \end{description}
neuper@37949: 
neuper@52155: The above rulesets are all visible to the user, and also may be input; 
neuper@52155: thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
neuper@52155: KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
s1210629013@55444: using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
neuper@37949: The following rulesets are used for internal purposes and usually invisible to the (naive) user:
neuper@37949: \begin{description}
neuper@37949: 
neuper@37949: \item [*\_erls] TODO
neuper@37949: \item [*\_prls] 
neuper@37949: \item [*\_srls] 
neuper@37949: 
neuper@37949: \end{description}
wneuper@59416: {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
neuper@37949: *}
neuper@37946: 
neuper@37946: ML {*
neuper@37972: val thy = @{theory};
neuper@37949: 
neuper@37949: (** evaluation of numerals and special predicates on the meta-level **)
neuper@37949: (*-------------------------functions---------------------*)
neuper@37949: local (* rlang 09.02 *)
neuper@37949:     (*.a 'c is coefficient of v' if v does occur in c.*)
wneuper@59389:     fun coeff_in v c = member op = (TermC.vars c) v;
neuper@37949: in
neuper@37949:     fun occurs_in v t = coeff_in v t;
neuper@37949: end;
neuper@37949: 
neuper@37949: (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
neuper@37949: fun eval_occurs_in _ "Atools.occurs'_in"
neuper@37949: 	     (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
wneuper@59416:     ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
wneuper@59416:      tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
neuper@37949:      if occurs_in v t
wneuper@59416:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59390: 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59416:     else SOME ((Rule.term2str p) ^ " = False",
wneuper@59390: 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
neuper@37949:   | eval_occurs_in _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)   
neuper@37949: fun some_occur_in vs t = 
neuper@37949:     let fun occurs_in' a b = occurs_in b a
neuper@37949:     in foldl or_ (false, map (occurs_in' t) vs) end;
neuper@37949: 
neuper@37949: (*("some_occur_in", ("Atools.some'_occur'_in", 
neuper@37949: 			eval_some_occur_in "#eval_some_occur_in_"))*)
neuper@37949: fun eval_some_occur_in _ "Atools.some'_occur'_in"
neuper@37949: 			  (p as (Const ("Atools.some'_occur'_in",_) 
neuper@37949: 				       $ vs $ t)) _ =
wneuper@59389:     if some_occur_in (TermC.isalist2list vs) t
wneuper@59416:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59416:     else SOME ((Rule.term2str p) ^ " = False",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37949:   | eval_some_occur_in _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: 
neuper@37949: 
neuper@37949: 
neuper@37949: (*evaluate 'is_atom'*)
neuper@37949: (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
neuper@37949: fun eval_is_atom (thmid:string) "Atools.is'_atom"
neuper@37949: 		 (t as (Const(op0,_) $ arg)) thy = 
neuper@37949:     (case arg of 
wneuper@59392: 	 Free (n,_) => SOME (TermC.mk_thmid thmid n "", 
wneuper@59390: 			      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59392:        | _ => SOME (TermC.mk_thmid thmid "" "", 
wneuper@59390: 		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
neuper@37949:   | eval_is_atom _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: (*evaluate 'is_even'*)
neuper@37949: fun even i = (i div 2) * 2 = i;
neuper@37949: (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
neuper@37949: fun eval_is_even (thmid:string) "Atools.is'_even"
neuper@37949: 		 (t as (Const(op0,_) $ arg)) thy = 
neuper@37949:     (case arg of 
neuper@37949: 	Free (n,_) =>
wneuper@59390: 	 (case TermC.int_of_str_opt n of
neuper@37949: 	      SOME i =>
wneuper@59392: 	      if even i then SOME (TermC.mk_thmid thmid n "", 
wneuper@59390: 				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59392: 	      else SOME (TermC.mk_thmid thmid "" "", 
wneuper@59390: 			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@37949: 	    | _ => NONE)
neuper@37949:        | _ => NONE)
neuper@37949:   | eval_is_even _ _ _ _ = NONE; 
neuper@37949: 
neuper@37949: (*evaluate 'is_const'*)
neuper@37949: (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
neuper@37949: fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
neuper@37949: 	       (t as (Const(op0,t0) $ arg)) (thy:theory) = 
neuper@37949:     (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
neuper@37949:     (case arg of 
neuper@37949:        Const (n1,_) =>
wneuper@59392: 	 SOME (TermC.mk_thmid thmid n1 "", 
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@37949:      | Free (n1,_) =>
wneuper@59390: 	 if TermC.is_num' n1
wneuper@59392: 	   then SOME (TermC.mk_thmid thmid n1 "", 
wneuper@59390: 		      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59392: 	 else SOME (TermC.mk_thmid thmid n1 "", 
wneuper@59390: 		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@37949:      | Const ("Float.Float",_) =>
wneuper@59416:        SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
wneuper@59390: 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
neuper@37949:      | _ => (*NONE*)
wneuper@59416:        SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
wneuper@59390: 		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
neuper@37949:   | eval_const _ _ _ _ = NONE; 
neuper@37949: 
neuper@37949: (*. evaluate binary, associative, commutative operators: *,+,^ .*)
neuper@38014: (*("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
neuper@38034:   ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
neuper@37949:   ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
neuper@37949: 
neuper@37949: (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
neuper@37949:        ("xxxxxx",op_,t,thy);
neuper@37949:    *)
neuper@55487: fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
neuper@55487:   thmid ^ "Float ((" ^ 
neuper@55487:   (string_of_int v11)^","^(string_of_int v12)^"), ("^
neuper@55487:   (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
neuper@55487:   (string_of_int v21)^","^(string_of_int v22)^"), ("^
neuper@55487:   (string_of_int p21)^","^(string_of_int p22)^"))";
neuper@37949: 
neuper@37949: (*.convert int and float to internal floatingpoint prepresentation.*)
neuper@37949: fun numeral (Free (str, T)) = 
wneuper@59390:     (case TermC.int_of_str_opt str of
neuper@37949: 	 SOME i => SOME ((i, 0), (0, 0))
neuper@37949:        | NONE => NONE)
neuper@37949:   | numeral (Const ("Float.Float", _) $
neuper@41972: 		   (Const ("Product_Type.Pair", _) $
neuper@41972: 			  (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
neuper@41972: 			  (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
wneuper@59390:     (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
neuper@37949: 	(SOME v1', SOME v2', SOME p1', SOME p2') =>
neuper@37949: 	SOME ((v1', v2'), (p1', p2'))
neuper@37949:       | _ => NONE)
neuper@37949:   | numeral _ = NONE;
neuper@37949: 
neuper@55487: (* evaluate binary associative operations *)
neuper@55487: fun eval_binop (thmid : string) (op_: string) 
neuper@55487:       (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ =  (* binary . (v.n1).n2 *)
neuper@37949:     if op0 = op0' then
neuper@55487:       case (numeral t1, numeral t2) of
neuper@55487:         (SOME n1, SOME n2) =>
neuper@55487:           let 
wneuper@59389:             val (T1, _, _) = TermC.dest_binop_typ t0
neuper@55487:             val res = 
neuper@55490:               calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
wneuper@59360:               (*WN071229 "Rings.divide_class.divide" never tried*)
neuper@55487:             val rhs = var_op_float v op_ t0 T1 res
wneuper@59390:             val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
wneuper@59416:           in SOME ("#: " ^ Rule.term2str prop, prop) end
neuper@55487:       | _ => NONE
neuper@37949:     else NONE
neuper@55487:   | eval_binop (thmid : string) (op_ : string) 
neuper@55487:       (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =  (* binary . n1.(n2.v) *)
neuper@55487:     if op0 = op0' then
neuper@55487:       case (numeral t1, numeral t2) of
neuper@55487:         (SOME n1, SOME n2) =>
neuper@55487:           if op0 = "Groups.minus_class.minus" then NONE 
neuper@55487:           else let 
wneuper@59389:             val (T1, _, _) = TermC.dest_binop_typ t0
neuper@55490:             val res = calcul op0 n1 n2
neuper@55487:             val rhs = float_op_var v op_ t0 T1 res
wneuper@59390:             val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
wneuper@59416:           in SOME ("#: " ^ Rule.term2str prop, prop) end
neuper@55487:       | _ => NONE
neuper@55487:     else NONE
neuper@55487:   | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ =   (* binary . n1.n2 *)
neuper@37949:     (case (numeral t1, numeral t2) of
neuper@55487:       (SOME n1, SOME n2) =>
neuper@55487:         let 
wneuper@59389:           val (_, _, Trange) = TermC.dest_binop_typ t0;
neuper@55490:           val res = calcul op0 n1 n2;
neuper@55487:           val rhs = term_of_float Trange res;
wneuper@59390:           val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
wneuper@59416:         in SOME ("#: " ^ Rule.term2str prop, prop) end
neuper@55487:     | _ => NONE)
neuper@37949:   | eval_binop _ _ _ _ = NONE; 
neuper@37949: (*
neuper@38014: > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
wneuper@59416: > Rule.term2str t;
neuper@37949: val it = "-1 + 2 = 1"
neuper@37949: > val t = str2term "-1 * (-1 * a)";
neuper@38034: > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
wneuper@59416: > Rule.term2str t;
neuper@37949: val it = "-1 * (-1 * a) = 1 * a"*)
neuper@37949: 
neuper@37949: 
neuper@37949: 
neuper@37949: (*.evaluate < and <= for numerals.*)
neuper@38045: (*("le"      ,("Orderings.ord_class.less"        ,eval_equ "#less_")),
neuper@38045:   ("leq"     ,("Orderings.ord_class.less_eq"       ,eval_equ "#less_equal_"))*)
neuper@37949: fun eval_equ (thmid:string) (op_:string) (t as 
neuper@37949: 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
wneuper@59390:     (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
neuper@37949: 	 (SOME n1', SOME n2') =>
wneuper@59401:   if Calc.calc_equ (strip_thy op0) (n1', n2')
wneuper@59392:     then SOME (TermC.mk_thmid thmid n1 n2, 
wneuper@59390: 	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59392:   else SOME (TermC.mk_thmid thmid n1 n2,  
wneuper@59390: 	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@37949:        | _ => NONE)
neuper@37949:     
neuper@37949:   | eval_equ _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: 
neuper@37949: (*evaluate identity
neuper@37949: > reflI;
neuper@37949: val it = "(?t = ?t) = True"
neuper@37949: > val t = str2term "x = 0";
wneuper@59416: > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
neuper@37949: 
neuper@37949: > val t = str2term "1 = 0";
wneuper@59416: > val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
wneuper@59416: ----------- thus needs Rule.Calc !
neuper@37949: > val t = str2term "0 = 0";
wneuper@59416: > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
wneuper@59416: > Rule.term2str t';
neuper@41928: val it = "HOL.True"
neuper@37949: 
neuper@37949: val t = str2term "Not (x = 0)";
wneuper@59416: atomt t; Rule.term2str t;
neuper@37949: *** -------------
neuper@37949: *** Const ( Not)
neuper@37949: *** . Const ( op =)
neuper@37949: *** . . Free ( x, )
neuper@37949: *** . . Free ( 0, )
neuper@37949: val it = "x ~= 0" : string*)
neuper@37949: 
neuper@37949: (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of 
neuper@37949:   the arguments: thus special handling by 'fun eval_binop'*)
neuper@37949: (*("ident"   ,("Atools.ident",eval_ident "#ident_")):calc*)
neuper@37949: fun eval_ident (thmid:string) "Atools.ident" (t as 
neuper@37949: 	       (Const (op0,t0) $ t1 $ t2 )) thy = 
neuper@37949:   if t1 = t2
wneuper@59392:   then SOME (TermC.mk_thmid thmid 
wneuper@59416: 	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
wneuper@59416: 	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"), 
wneuper@59390: 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59392:   else SOME (TermC.mk_thmid thmid  
wneuper@59416: 	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
wneuper@59416: 	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),  
wneuper@59390: 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@37949:   | eval_ident _ _ _ _ = NONE;
neuper@37949: (* TODO
neuper@37949: > val t = str2term "x =!= 0";
neuper@37949: > val SOME (str, t') = eval_ident "ident_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "ident_(x)_(0)" : string
neuper@37949: val it = "(x =!= 0) = False" : string                                
neuper@37949: > val t = str2term "1 =!= 0";
neuper@37949: > val SOME (str, t') = eval_ident "ident_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "ident_(1)_(0)" : string 
neuper@37949: val it = "(1 =!= 0) = False" : string                                       
neuper@37949: > val t = str2term "0 =!= 0";
neuper@37949: > val SOME (str, t') = eval_ident "ident_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "ident_(0)_(0)" : string
neuper@37949: val it = "(0 =!= 0) = True" : string
neuper@37949: *)
neuper@37949: 
neuper@37949: (*.evaluate identity of terms, which stay ready for evaluation in turn;
neuper@37949:   thus returns False only for atoms.*)
neuper@41922: (*("equal"   ,("HOL.eq",eval_equal "#equal_")):calc*)
neuper@52070: fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy = 
neuper@52070:   if t1 = t2
wneuper@59392:   then SOME (TermC.mk_thmid thmid 
wneuper@59416:                 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
wneuper@59416:                 ("(" ^ Rule.term_to_string''' thy t2 ^ ")"), 
wneuper@59390:        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59389:   else (case (TermC.is_atom t1, TermC.is_atom t2) of
neuper@52070:       (true, true) => 
wneuper@59392:       SOME (TermC.mk_thmid thmid  
wneuper@59416:          ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
wneuper@59416:          ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
wneuper@59390:       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@52070:     | _ => NONE)                             (* NOT is_atom t1,t2 --> rew_sub *)
neuper@38053:   | eval_equal _ _ _ _ = NONE;                                  (* error-exit *)
neuper@37949: (*
neuper@37949: val t = str2term "x ~= 0";
neuper@37949: val NONE = eval_equal "equal_" "b" t thy;
neuper@37949: 
neuper@37949: 
neuper@37949: > val t = str2term "(x + 1) = (x + 1)";
neuper@37949: > val SOME (str, t') = eval_equal "equal_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "equal_(x + 1)_(x + 1)" : string
neuper@37949: val it = "(x + 1 = x + 1) = True" : string
neuper@37949: > val t = str2term "x = 0";
neuper@37949: > val NONE = eval_equal "equal_" "b" t thy;
neuper@37949: 
neuper@37949: > val t = str2term "1 = 0";
neuper@37949: > val SOME (str, t') = eval_equal "equal_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "equal_(1)_(0)" : string 
neuper@37949: val it = "(1 = 0) = False" : string
neuper@37949: > val t = str2term "0 = 0";
neuper@37949: > val SOME (str, t') = eval_equal "equal_" "b" t thy;
wneuper@59416: > Rule.term2str t';
neuper@37949: val str = "equal_(0)_(0)" : string
neuper@37949: val it = "(0 = 0) = True" : string
neuper@37949: *)
neuper@37949: 
neuper@37949: 
neuper@42451: *}
neuper@42451: 
neuper@42451: ML {*
neuper@37949: (** evaluation on the metalevel **)
neuper@37949: 
neuper@37949: (*. evaluate HOL.divide .*)
wneuper@59360: (*("DIVIDE" ,("Rings.divide_class.divide"  ,eval_cancel "#divide_e"))*)
wneuper@59360: fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as 
neuper@37949: 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
wneuper@59390:     (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
neuper@37949: 	 (SOME n1', SOME n2') =>
neuper@37949:   let 
wneuper@59401:     val sg = Calc.sign_mult n1' n2';
wneuper@59389:     val (T1,T2,Trange) = TermC.dest_binop_typ t0;
wneuper@59401:     val gcd' = Calc.gcd (abs n1') (abs n2');
neuper@37949:   in if gcd' = abs n2' 
wneuper@59389:      then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
wneuper@59390: 	      val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
wneuper@59392: 	  in SOME (TermC.mk_thmid thmid n1 n2, prop) end     
neuper@37949:      else if 0 < n2' andalso gcd' = 1 then NONE
wneuper@59390:      else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
neuper@37949: 				   ((abs n2') div gcd')
wneuper@59390: 	      val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
wneuper@59392: 	  in SOME (TermC.mk_thmid thmid n1 n2, prop) end
neuper@37949:   end
neuper@38015:        | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
neuper@37949: 
neuper@37949:   | eval_cancel _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: (*. get the argument from a function-definition.*)
neuper@37949: (*("argument_in" ,("Atools.argument'_in",
neuper@37949: 		   eval_argument_in "Atools.argument'_in"))*)
neuper@37949: fun eval_argument_in _ "Atools.argument'_in" 
neuper@37949: 		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
neuper@37949:     if is_Free arg (*could be something to be simplified before*)
wneuper@59416:     then SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
neuper@37949:     else NONE
neuper@37949:   | eval_argument_in _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: (*.check if the function-identifier of the first argument matches 
neuper@37949:    the function-identifier of the lhs of the second argument.*)
neuper@37949: (*("sameFunId" ,("Atools.sameFunId",
neuper@37949: 		   eval_same_funid "Atools.sameFunId"))*)
neuper@37949: fun eval_sameFunId _ "Atools.sameFunId" 
neuper@37949: 		     (p as Const ("Atools.sameFunId",_) $ 
neuper@37949: 			(f1 $ _) $ 
neuper@41922: 			(Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
neuper@37949:     if f1 = f2 
wneuper@59416:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59416:     else SOME ((Rule.term2str p) ^ " = False",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37949: | eval_sameFunId _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: 
neuper@37949: (*.from a list of fun-definitions "f x = ..." as 2nd argument
neuper@37949:    filter the elements with the same fun-identfier in "f y"
neuper@37949:    as the fst argument;
neuper@37949:    this is, because Isabelles filter takes more than 1 sec.*)
neuper@41922: fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
neuper@38031:   | same_funid f1 t = error ("same_funid called with t = ("
wneuper@59416: 				   ^Rule.term2str f1^") ("^Rule.term2str t^")");
neuper@37949: (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
neuper@37949: 		   eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
neuper@37949: fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" 
neuper@37949: 		     (p as Const ("Atools.filter'_sameFunId",_) $ 
neuper@37949: 			(fid $ _) $ fs) _ =
wneuper@59389:     let val fs' = ((TermC.list2isalist HOLogic.boolT) o 
wneuper@59389: 		   (filter (same_funid fid))) (TermC.isalist2list fs)
wneuper@59416:     in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
neuper@37949: | eval_filter_sameFunId _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: 
neuper@37949: (*make a list of terms to a sum*)
neuper@37949: fun list2sum [] = error ("list2sum called with []")
neuper@37949:   | list2sum [s] = s
neuper@37949:   | list2sum (s::ss) = 
neuper@37949:     let fun sum su [s'] = 
neuper@38014: 	    Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
neuper@37949: 		  $ su $ s'
neuper@37949: 	  | sum su (s'::ss') = 
neuper@38014: 	    sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
neuper@37949: 		  $ su $ s') ss'
neuper@37949:     in sum s ss end;
neuper@37949: 
neuper@37949: (*make a list of equalities to the sum of the lhs*)
neuper@37949: (*("boollist2sum"    ,("Atools.boollist2sum"    ,eval_boollist2sum "")):calc*)
neuper@37949: fun eval_boollist2sum _ "Atools.boollist2sum" 
neuper@37949: 		      (p as Const ("Atools.boollist2sum", _) $ 
neuper@37949: 			 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
wneuper@59389:     let val isal = TermC.isalist2list l
neuper@37949: 	val lhss = map lhs isal
neuper@37949: 	val sum = list2sum lhss
wneuper@59416:     in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
wneuper@59390: 	  HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
neuper@37949:     end
neuper@37949: | eval_boollist2sum _ _ _ _ = NONE;
neuper@37949: 
neuper@37949: 
neuper@37949: 
neuper@37949: local
neuper@37949: 
neuper@37949: open Term;
neuper@37949: 
neuper@37949: in
wneuper@59416: fun termlessI (_: Rule.subst) uv = Term_Ord.termless uv;
wneuper@59416: fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
neuper@37949: end;
neuper@37949: 
neuper@37949: 
neuper@37949: (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
neuper@37949: 
neuper@37949: 
wneuper@59416: val list_rls = Rule.append_rls "list_rls" list_rls
wneuper@59416: 	 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
wneuper@59416: 		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
wneuper@59416: 		Rule.Calc ("Atools.ident",eval_ident "#ident_"),
wneuper@59416: 		Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
neuper@37949:        
wneuper@59416: 		Rule.Calc ("Tools.Vars",eval_var "#Vars_"),
neuper@37949: 		
wneuper@59416: 		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
wneuper@59416: 		Rule.Thm ("if_False",TermC.num_str @{thm if_False})
neuper@37949: 		];
neuper@52125: *}
neuper@52125: ML {*
neuper@37949: 
wneuper@59416: (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
wneuper@59416: val tless_true = Rule.dummy_ord;
wneuper@59416: Rule.rew_ord' := overwritel (! Rule.rew_ord',
neuper@37949: 			[("tless_true", tless_true),
neuper@37949: 			 ("e_rew_ord'", tless_true),
wneuper@59416: 			 ("dummy_ord", Rule.dummy_ord)]);
neuper@37949: 
wneuper@59424: val calculate_Base_Tools = 
wneuper@59416:     Rule.append_rls "calculate_Atools" Rule.e_rls
wneuper@59416:                [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
wneuper@59416: 		Rule.Calc ("HOL.eq",eval_equal "#equal_"),
neuper@37949: 
wneuper@59416: 		Rule.Thm  ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
wneuper@59416: 		Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
wneuper@59416: 		Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
wneuper@59416: 		Rule.Calc ("Groups.times_class.times",eval_binop "#mult_")
neuper@37949: 		];
neuper@37949: 
neuper@42451: *}
neuper@42451: 
neuper@48763: find_theorems (9) "?n <= ?n"
neuper@48763: 
neuper@42451: ML {*
neuper@37949: val Atools_erls = 
wneuper@59416:     Rule.append_rls "Atools_erls" Rule.e_rls
wneuper@59416:                [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
wneuper@59416:                 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
neuper@37949: 		(*"(~ True) = False"*)
wneuper@59416: 		Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
neuper@37949: 		(*"(~ False) = True"*)
wneuper@59416: 		Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
neuper@37949: 		(*"(?a & True) = ?a"*)
wneuper@59416: 		Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
neuper@37949: 		(*"(?a & False) = False"*)
wneuper@59416: 		Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
neuper@37949: 		(*"(?a | True) = True"*)
wneuper@59416: 		Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
neuper@37949: 		(*"(?a | False) = ?a"*)
neuper@37949:                
wneuper@59416: 		Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
wneuper@59416: 		Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
wneuper@59416: 		Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
wneuper@59416:                 Rule.Thm ("refl",TermC.num_str @{thm refl}),
wneuper@59416: 		Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
wneuper@59416: 		Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Atools.ident",eval_ident "#ident_"),    
wneuper@59416: 		Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 		Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
wneuper@59416: 		Rule.Calc ("Tools.matches",eval_matches "")
neuper@37949: 		];
neuper@37949: 
neuper@42451: *}
neuper@42451: 
neuper@42451: ML {*
neuper@37949: val Atools_crls = 
wneuper@59416:     Rule.append_rls "Atools_crls" Rule.e_rls
wneuper@59416:                [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
wneuper@59416:                 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
wneuper@59416: 		Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
wneuper@59416: 		Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
wneuper@59416: 		Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
wneuper@59416: 		Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
wneuper@59416: 		Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
neuper@37949:                
wneuper@59416: 		Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
wneuper@59416: 		Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
wneuper@59416: 		Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
wneuper@59416:                 Rule.Thm ("refl",TermC.num_str @{thm refl}),
wneuper@59416: 		Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
wneuper@59416: 		Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Atools.ident",eval_ident "#ident_"),    
wneuper@59416: 		Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 		Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
wneuper@59416: 		Rule.Calc ("Tools.matches",eval_matches "")
neuper@37949: 		];
neuper@37949: 
neuper@37949: (*val atools_erls = ... waere zu testen ...
wneuper@59416:     Rule.merge_rls calculate_Atools
wneuper@59416: 	      (Rule.append_rls Atools_erls (*i.A. zu viele rules*)
wneuper@59416: 			  [Rule.Calc ("Atools.ident",eval_ident "#ident_"),    
wneuper@59416: 			   Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 			   Rule.Calc ("Atools.occurs'_in",
neuper@37949: 				 eval_occurs_in "#occurs_in"),    
wneuper@59416: 			   Rule.Calc ("Tools.matches",eval_matches "#matches")
neuper@37949: 			   ] (*i.A. zu viele rules*)
neuper@37949: 			  );*)
s1210629013@55444: (* val atools_erls = prep_rls'(     (*outcommented*)
wneuper@59416:   Rule.Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), 
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("refl",num_str @{thm refl}),
wneuper@59416: 		Rule.Thm ("order_refl",num_str @{thm order_refl}),
wneuper@59416: 		Rule.Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
wneuper@59416: 		Rule.Thm ("not_true",num_str @{thm not_true}),
wneuper@59416: 		Rule.Thm ("not_false",num_str @{thm not_false}),
wneuper@59416: 		Rule.Thm ("and_true",num_str @{thm and_true}),
wneuper@59416: 		Rule.Thm ("and_false",num_str @{thm and_false}),
wneuper@59416: 		Rule.Thm ("or_true",num_str @{thm or_true}),
wneuper@59416: 		Rule.Thm ("or_false",num_str @{thm or_false}),
wneuper@59416: 		Rule.Thm ("and_commute",num_str @{thm and_commute}),
wneuper@59416: 		Rule.Thm ("or_commute",num_str @{thm or_commute}),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
neuper@37949: 		
wneuper@59416: 		Rule.Calc ("Atools.ident",eval_ident "#ident_"),    
wneuper@59416: 		Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 		Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
wneuper@59416: 		Rule.Calc ("Tools.matches",eval_matches "")
neuper@37949: 	       ],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
wneuper@59406:       });
neuper@37949: *)
neuper@37949: "******* Atools.ML end *******";
s1210629013@52145: *}
s1210629013@52145: setup {* KEStore_Elems.add_calcs
s1210629013@52145:   [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
s1210629013@52145:     ("some_occur_in",
s1210629013@52145:       ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
s1210629013@52145:     ("is_atom"  ,("Atools.is'_atom", eval_is_atom "#is_atom_")),
s1210629013@52145:     ("is_even"  ,("Atools.is'_even", eval_is_even "#is_even_")),
s1210629013@52145:     ("is_const" ,("Atools.is'_const", eval_const "#is_const_")),
s1210629013@52145:     ("le"       ,("Orderings.ord_class.less", eval_equ "#less_")),
s1210629013@52145:     ("leq"      ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
s1210629013@52145:     ("ident"    ,("Atools.ident", eval_ident "#ident_")),
s1210629013@52145:     ("equal"    ,("HOL.eq", eval_equal "#equal_")),
s1210629013@52145:     ("PLUS"     ,("Groups.plus_class.plus", eval_binop "#add_")),
s1210629013@52145:     ("MINUS"    ,("Groups.minus_class.minus", eval_binop "#sub_")),
s1210629013@52145:     ("TIMES"    ,("Groups.times_class.times", eval_binop "#mult_")),
wneuper@59360:     ("DIVIDE"  ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
s1210629013@52145:     ("POWER"   ,("Atools.pow", eval_binop "#power_")),
s1210629013@52145:     ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
s1210629013@52145: ML {*
wneuper@59416: val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
wneuper@59416: 	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
wneuper@59416:     erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
wneuper@59416:         Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
neuper@52139:         (*    ~~~~~~ for nth_Cons_*)],
wneuper@59416:       scr = Rule.EmptyScr},
wneuper@59416:     srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:     rules = [], scr = Rule.EmptyScr})
neuper@52139:   list_rls);
neuper@37946: *}
neuper@52139: setup {* KEStore_Elems.add_rlss
wneuper@59375:   [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))] *}
neuper@48764: 
neuper@37906: end