(* Title:  tools for arithmetic

    Author: Walther Neuper 010308

    (c) due to copyright terms

 remove_thy"Atools";

 use_thy"Knowledge/Atools";

 use_thy"Knowledge/Isac";

 use_thy_only"Knowledge/Atools";

 use_thy"Knowledge/Isac";

 *)

 theory Atools imports Descript Typefix begin

 consts

   Arbfix           :: "real"

   Undef            :: "real"

   dummy            :: "real"

   some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")

   occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")

   pow              :: "[real, real] => real"    (infixr "^^^" 80)

 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)

                            ~~~~     ~~~~    ~~~~     ~~~*)

 (*WN0603 at Frontend encoded strings to '^', 

 	see 'fun encode', fun 'decode'*)

   abs              :: "real => real"            ("(|| _ ||)")

 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)

   absset           :: "real set => real"        ("(||| _ |||)")

   (*is numeral constant ?*)

   is'_const        :: "real => bool"            ("_ is'_const" 10)

   (*is_const rename to is_num FIXXXME.WN.16.5.03 *)

   is'_atom         :: "real => bool"            ("_ is'_atom" 10)

   is'_even         :: "real => bool"            ("_ is'_even" 10)

   (* identity on term level*)

   ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)

   argument'_in     :: "real => real"            ("argument'_in _" 10)

   sameFunId        :: "[real, bool] => bool"    (**"same'_funid _ _" 10

 	WN0609 changed the id, because ".. _ _" inhibits currying**)

   filter'_sameFunId:: "[real, bool list] => bool list" 

 					        ("filter'_sameFunId _ _" 10)

   boollist2sum     :: "bool list => real"

 axioms (*for evaluating the assumptions of conditional rules*)

   last_thmI	      "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"

   real_unari_minus    "- a = (-1) * a"           (*Isa!*)

   rle_refl            "(n::real) <= n"

 (*reflI               "(t = t) = True"*)

   radd_left_cancel_le "((k::real) + m <= k + n) = (m <= n)"

   not_true            "(~ True) = False"

   not_false           "(~ False) = True"

   and_true            "(a & True) = a"

   and_false           "(a & False) = False"

   or_true             "(a | True) = True"

   or_false            "(a | False) = a"

   and_commute         "(a & b) = (b & a)"

   or_commute          "(a | b) = (b | a)"

   (*.should be in Rational.thy, but: 

    needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)

   rat_leq1	      "[| b ~= 0; d ~= 0 |] ==> \

 		      \((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)

   rat_leq2	      "d ~= 0 ==> \

 		      \( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*)

   rat_leq3	      "b ~= 0 ==> \

 		      \((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)

 text {*copy from doc/math-eng.tex WN.28.3.03

 WN071228 extended *}

 section {*Coding standards*}

 subsection {*Identifiers*}

 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).

 This are the preliminary rules for naming identifiers>

 \begin{description}

 \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}.

 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.

 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!

 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.

 \item [???] ???

 \item [???] ???

 \end{description}

 %WN071228 extended *}

 subsection {*Rule sets*}

 text {*The actual version of the coding standards for rulesets is in {\tt /Knowledge/Atools.ML where it can be viewed using the knowledge browsers.

 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.

 \begin{description}

 \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).

 \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.

 \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.

 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).

 \end{description}

 The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.

 The following rulesets are used for internal purposes and usually invisible to the (naive) user:

 \begin{description}

 \item [*\_erls] 

 \item [*\_prls] 

 \item [*\_srls] 

 \end{description}

 {\tt append_rls, merge_rls, remove_rls}

 *}

 ML {*

 (** evaluation of numerals and special predicates on the meta-level **)

 (*-------------------------functions---------------------*)

 local (* rlang 09.02 *)

     (*.a 'c is coefficient of v' if v does occur in c.*)

     fun coeff_in v c = member op = (vars c) v;

 in

     fun occurs_in v t = coeff_in v t;

 end;

 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)

 fun eval_occurs_in _ "Atools.occurs'_in"

 	     (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =

     ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));

      writeln("@@@ eval_occurs_in: t= "^(term2str t));*)

      if occurs_in v t

     then SOME ((term2str p) ^ " = True",

 	  Trueprop $ (mk_equality (p, HOLogic.true_const)))

     else SOME ((term2str p) ^ " = False",

 	  Trueprop $ (mk_equality (p, HOLogic.false_const))))

   | eval_occurs_in _ _ _ _ = NONE;

 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)   

 fun some_occur_in vs t = 

     let fun occurs_in' a b = occurs_in b a

     in foldl or_ (false, map (occurs_in' t) vs) end;

 (*("some_occur_in", ("Atools.some'_occur'_in", 

 			eval_some_occur_in "#eval_some_occur_in_"))*)

 fun eval_some_occur_in _ "Atools.some'_occur'_in"

 			  (p as (Const ("Atools.some'_occur'_in",_) 

 				       $ vs $ t)) _ =

     if some_occur_in (isalist2list vs) t

     then SOME ((term2str p) ^ " = True",

 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))

     else SOME ((term2str p) ^ " = False",

 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

   | eval_some_occur_in _ _ _ _ = NONE;

 (*evaluate 'is_atom'*)

 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)

 fun eval_is_atom (thmid:string) "Atools.is'_atom"

 		 (t as (Const(op0,_) $ arg)) thy = 

     (case arg of 

 	 Free (n,_) => SOME (mk_thmid thmid op0 n "", 

 			      Trueprop $ (mk_equality (t, true_as_term)))

        | _ => SOME (mk_thmid thmid op0 "" "", 

 		    Trueprop $ (mk_equality (t, false_as_term))))

   | eval_is_atom _ _ _ _ = NONE;

 (*evaluate 'is_even'*)

 fun even i = (i div 2) * 2 = i;

 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)

 fun eval_is_even (thmid:string) "Atools.is'_even"

 		 (t as (Const(op0,_) $ arg)) thy = 

     (case arg of 

 	Free (n,_) =>

 	 (case int_of_str n of

 	      SOME i =>

 	      if even i then SOME (mk_thmid thmid op0 n "", 

 				   Trueprop $ (mk_equality (t, true_as_term)))

 	      else SOME (mk_thmid thmid op0 "" "", 

 			 Trueprop $ (mk_equality (t, false_as_term)))

 	    | _ => NONE)

        | _ => NONE)

   | eval_is_even _ _ _ _ = NONE; 

 (*evaluate 'is_const'*)

 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)

 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)

 	       (t as (Const(op0,t0) $ arg)) (thy:theory) = 

     (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)

     (case arg of 

        Const (n1,_) =>

 	 SOME (mk_thmid thmid op0 n1 "", 

 	       Trueprop $ (mk_equality (t, false_as_term)))

      | Free (n1,_) =>

 	 if is_numeral n1

 	   then SOME (mk_thmid thmid op0 n1 "", 

 		      Trueprop $ (mk_equality (t, true_as_term)))

 	 else SOME (mk_thmid thmid op0 n1 "", 

 		    Trueprop $ (mk_equality (t, false_as_term)))

      | Const ("Float.Float",_) =>

        SOME (mk_thmid thmid op0 (term2str arg) "", 

 	     Trueprop $ (mk_equality (t, true_as_term)))

      | _ => (*NONE*)

        SOME (mk_thmid thmid op0 (term2str arg) "", 

 		    Trueprop $ (mk_equality (t, false_as_term))))

   | eval_const _ _ _ _ = NONE; 

 (*. evaluate binary, associative, commutative operators: *,+,^ .*)

 (*("PLUS"    ,("op +"        ,eval_binop "#add_")),

   ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

   ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)

 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =

        ("xxxxxx",op_,t,thy);

    *)

 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22))  = 

     thmid ^ "Float ((" ^ 

     (string_of_int v11)^","^(string_of_int v12)^"), ("^

     (string_of_int p11)^","^(string_of_int p12)^")) __ (("^

     (string_of_int v21)^","^(string_of_int v22)^"), ("^

     (string_of_int p21)^","^(string_of_int p22)^"))";

 (*.convert int and float to internal floatingpoint prepresentation.*)

 fun numeral (Free (str, T)) = 

     (case int_of_str str of

 	 SOME i => SOME ((i, 0), (0, 0))

        | NONE => NONE)

   | numeral (Const ("Float.Float", _) $

 		   (Const ("Pair", _) $

 			  (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $

 			  (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=

     (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of

 	(SOME v1', SOME v2', SOME p1', SOME p2') =>

 	SOME ((v1', v2'), (p1', p2'))

       | _ => NONE)

   | numeral _ = NONE;

 (*.evaluate binary associative operations.*)

 fun eval_binop (thmid:string) (op_:string) 

 	       (t as ( Const(op0,t0) $ 

 			    (Const(op0',t0') $ v $ t1) $ t2)) 

 	       thy =                                     (*binary . (v.n1).n2*)

     if op0 = op0' then

 	case (numeral t1, numeral t2) of

 	    (SOME n1, SOME n2) =>

 	    let val (T1,T2,Trange) = dest_binop_typ t0

 		val res = calc (if op0 = "op -" then "op +" else op0) n1 n2

 		(*WN071229 "HOL.divide" never tried*)

 		val rhs = var_op_float v op_ t0 T1 res

 		val prop = Trueprop $ (mk_equality (t, rhs))

 	    in SOME (mk_thmid_f thmid n1 n2, prop) end

 	  | _ => NONE

     else NONE

   | eval_binop (thmid:string) (op_:string) 

 	       (t as 

 		  (Const (op0, t0) $ t1 $ 

 			 (Const (op0', t0') $ t2 $ v))) 

 	       thy =                                     (*binary . n1.(n2.v)*)

   if op0 = op0' then

 	case (numeral t1, numeral t2) of

 	    (SOME n1, SOME n2) =>

 	    if op0 = "op -" then NONE else

 	    let val (T1,T2,Trange) = dest_binop_typ t0

 		val res = calc op0 n1 n2

 		val rhs = float_op_var v op_ t0 T1 res

 		val prop = Trueprop $ (mk_equality (t, rhs))

 	    in SOME (mk_thmid_f thmid n1 n2, prop) end

 	  | _ => NONE

   else NONE

   | eval_binop (thmid:string) (op_:string)

 	       (t as (Const (op0,t0) $ t1 $ t2)) thy =       (*binary . n1.n2*)

     (case (numeral t1, numeral t2) of

 	 (SOME n1, SOME n2) =>

 	 let val (T1,T2,Trange) = dest_binop_typ t0;

 	     val res = calc op0 n1 n2;

 	     val rhs = term_of_float Trange res;

 	     val prop = Trueprop $ (mk_equality (t, rhs));

 	 in SOME (mk_thmid_f thmid n1 n2, prop) end

        | _ => NONE)

   | eval_binop _ _ _ _ = NONE; 

 (*

 > val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;

 > term2str t;

 val it = "-1 + 2 = 1"

 > val t = str2term "-1 * (-1 * a)";

 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;

 > term2str t;

 val it = "-1 * (-1 * a) = 1 * a"*)

 (*.evaluate < and <= for numerals.*)

 (*("le"      ,("op <"        ,eval_equ "#less_")),

   ("leq"     ,("op <="       ,eval_equ "#less_equal_"))*)

 fun eval_equ (thmid:string) (op_:string) (t as 

 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 

     (case (int_of_str n1, int_of_str n2) of

 	 (SOME n1', SOME n2') =>

   if calc_equ (strip_thy op0) (n1', n2')

     then SOME (mk_thmid thmid op0 n1 n2, 

 	  Trueprop $ (mk_equality (t, true_as_term)))

   else SOME (mk_thmid thmid op0 n1 n2,  

 	  Trueprop $ (mk_equality (t, false_as_term)))

        | _ => NONE)

   | eval_equ _ _ _ _ = NONE;

 (*evaluate identity

 > reflI;

 val it = "(?t = ?t) = True"

 > val t = str2term "x = 0";

 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;

 > val t = str2term "1 = 0";

 > val NONE = rewrite_ thy dummy_ord e_rls false reflI t;

 ----------- thus needs Calc !

 > val t = str2term "0 = 0";

 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;

 > term2str t';

 val it = "True"

 val t = str2term "Not (x = 0)";

 atomt t; term2str t;

 *** -------------

 *** Const ( Not)

 *** . Const ( op =)

 *** . . Free ( x, )

 *** . . Free ( 0, )

 val it = "x ~= 0" : string*)

 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of 

   the arguments: thus special handling by 'fun eval_binop'*)

 (*("ident"   ,("Atools.ident",eval_ident "#ident_")):calc*)

 fun eval_ident (thmid:string) "Atools.ident" (t as 

 	       (Const (op0,t0) $ t1 $ t2 )) thy = 

   if t1 = t2

     then SOME (mk_thmid thmid op0 

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 

 	  Trueprop $ (mk_equality (t, true_as_term)))

   else SOME (mk_thmid thmid op0  

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),  

 	  Trueprop $ (mk_equality (t, false_as_term)))

   | eval_ident _ _ _ _ = NONE;

 (* TODO

 > val t = str2term "x =!= 0";

 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

 > term2str t';

 val str = "ident_(x)_(0)" : string

 val it = "(x =!= 0) = False" : string                                

 > val t = str2term "1 =!= 0";

 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

 > term2str t';

 val str = "ident_(1)_(0)" : string 

 val it = "(1 =!= 0) = False" : string                                       

 > val t = str2term "0 =!= 0";

 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

 > term2str t';

 val str = "ident_(0)_(0)" : string

 val it = "(0 =!= 0) = True" : string

 *)

 (*.evaluate identity of terms, which stay ready for evaluation in turn;

   thus returns False only for atoms.*)

 (*("equal"   ,("op =",eval_equal "#equal_")):calc*)

 fun eval_equal (thmid:string) "op =" (t as 

 	       (Const (op0,t0) $ t1 $ t2 )) thy = 

   if t1 = t2

     then ((*writeln"... eval_equal: t1 = t2  --> True";*)

 	  SOME (mk_thmid thmid op0 

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")

 	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 

 	  Trueprop $ (mk_equality (t, true_as_term)))

 	  )

   else (case (is_atom t1, is_atom t2) of

 	    (true, true) => 

 	    ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)

 	     SOME (mk_thmid thmid op0  

 			   ("("^(term2str t1)^")") ("("^(term2str t2)^")"),

 		  Trueprop $ (mk_equality (t, false_as_term)))

 	     )

 	  | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)

 		  NONE))

   | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";

 			  NONE);

 (*

 val t = str2term "x ~= 0";

 val NONE = eval_equal "equal_" "b" t thy;

 > val t = str2term "(x + 1) = (x + 1)";

 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

 > term2str t';

 val str = "equal_(x + 1)_(x + 1)" : string

 val it = "(x + 1 = x + 1) = True" : string

 > val t = str2term "x = 0";

 > val NONE = eval_equal "equal_" "b" t thy;

 > val t = str2term "1 = 0";

 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

 > term2str t';

 val str = "equal_(1)_(0)" : string 

 val it = "(1 = 0) = False" : string

 > val t = str2term "0 = 0";

 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

 > term2str t';

 val str = "equal_(0)_(0)" : string

 val it = "(0 = 0) = True" : string

 *)

 (** evaluation on the metalevel **)

 (*. evaluate HOL.divide .*)

 (*("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_"))*)

 fun eval_cancel (thmid:string) "HOL.divide" (t as 

 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 

     (case (int_of_str n1, int_of_str n2) of

 	 (SOME n1', SOME n2') =>

   let 

     val sg = sign2 n1' n2';

     val (T1,T2,Trange) = dest_binop_typ t0;

     val gcd' = gcd (abs n1') (abs n2');

   in if gcd' = abs n2' 

      then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')

 	      val prop = Trueprop $ (mk_equality (t, rhs))

 	  in SOME (mk_thmid thmid op0 n1 n2, prop) end     

      else if 0 < n2' andalso gcd' = 1 then NONE

      else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')

 				   ((abs n2') div gcd')

 	      val prop = Trueprop $ (mk_equality (t, rhs))

 	  in SOME (mk_thmid thmid op0 n1 n2, prop) end

   end

        | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))

   | eval_cancel _ _ _ _ = NONE;

 (*. get the argument from a function-definition.*)

 (*("argument_in" ,("Atools.argument'_in",

 		   eval_argument_in "Atools.argument'_in"))*)

 fun eval_argument_in _ "Atools.argument'_in" 

 		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =

     if is_Free arg (*could be something to be simplified before*)

     then SOME (term2str t ^ " = " ^ term2str arg,

 	       Trueprop $ (mk_equality (t, arg)))

     else NONE

   | eval_argument_in _ _ _ _ = NONE;

 (*.check if the function-identifier of the first argument matches 

    the function-identifier of the lhs of the second argument.*)

 (*("sameFunId" ,("Atools.sameFunId",

 		   eval_same_funid "Atools.sameFunId"))*)

 fun eval_sameFunId _ "Atools.sameFunId" 

 		     (p as Const ("Atools.sameFunId",_) $ 

 			(f1 $ _) $ 

 			(Const ("op =", _) $ (f2 $ _) $ _)) _ =

     if f1 = f2 

     then SOME ((term2str p) ^ " = True",

 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))

     else SOME ((term2str p) ^ " = False",

 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

 | eval_sameFunId _ _ _ _ = NONE;

 (*.from a list of fun-definitions "f x = ..." as 2nd argument

    filter the elements with the same fun-identfier in "f y"

    as the fst argument;

    this is, because Isabelles filter takes more than 1 sec.*)

 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2

   | same_funid f1 t = raise error ("same_funid called with t = ("

 				   ^term2str f1^") ("^term2str t^")");

 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",

 		   eval_filter_sameFunId "Atools.filter'_sameFunId"))*)

 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" 

 		     (p as Const ("Atools.filter'_sameFunId",_) $ 

 			(fid $ _) $ fs) _ =

     let val fs' = ((list2isalist HOLogic.boolT) o 

 		   (filter (same_funid fid))) (isalist2list fs)

     in SOME (term2str (mk_equality (p, fs')),

 	       Trueprop $ (mk_equality (p, fs'))) end

 | eval_filter_sameFunId _ _ _ _ = NONE;

 (*make a list of terms to a sum*)

 fun list2sum [] = error ("list2sum called with []")

   | list2sum [s] = s

   | list2sum (s::ss) = 

     let fun sum su [s'] = 

 	    Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

 		  $ su $ s'

 	  | sum su (s'::ss') = 

 	    sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

 		  $ su $ s') ss'

     in sum s ss end;

 (*make a list of equalities to the sum of the lhs*)

 (*("boollist2sum"    ,("Atools.boollist2sum"    ,eval_boollist2sum "")):calc*)

 fun eval_boollist2sum _ "Atools.boollist2sum" 

 		      (p as Const ("Atools.boollist2sum", _) $ 

 			 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =

     let val isal = isalist2list l

 	val lhss = map lhs isal

 	val sum = list2sum lhss

     in SOME ((term2str p) ^ " = " ^ (term2str sum),

 	  Trueprop $ (mk_equality (p, sum)))

     end

 | eval_boollist2sum _ _ _ _ = NONE;

 local

 open Term;

 in

 fun termlessI (_:subst) uv = termless uv;

 fun term_ordI (_:subst) uv = term_ord uv;

 end;

 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)

 val list_rls = 

     append_rls "list_rls" list_rls

 	       [Calc ("op *",eval_binop "#mult_"),

 		Calc ("op +", eval_binop "#add_"), 

 		Calc ("op <",eval_equ "#less_"),

 		Calc ("op <=",eval_equ "#less_equal_"),

 		Calc ("Atools.ident",eval_ident "#ident_"),

 		Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)

 		Calc ("Tools.Vars",eval_var "#Vars_"),

 		Thm ("if_True",num_str if_True),

 		Thm ("if_False",num_str if_False)

 		];

 ruleset' := overwritelthy thy (!ruleset',

   [("list_rls",list_rls)

    ]);

 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)

 val tless_true = dummy_ord;

 rew_ord' := overwritel (!rew_ord',

 			[("tless_true", tless_true),

 			 ("e_rew_ord'", tless_true),

 			 ("dummy_ord", dummy_ord)]);

 val calculate_Atools = 

     append_rls "calculate_Atools" e_rls

                [Calc ("op <",eval_equ "#less_"),

 		Calc ("op <=",eval_equ "#less_equal_"),

 		Calc ("op =",eval_equal "#equal_"),

 		Thm  ("real_unari_minus",num_str real_unari_minus),

 		Calc ("op +",eval_binop "#add_"),

 		Calc ("op -",eval_binop "#sub_"),

 		Calc ("op *",eval_binop "#mult_")

 		];

 val Atools_erls = 

     append_rls "Atools_erls" e_rls

                [Calc ("op =",eval_equal "#equal_"),

                 Thm ("not_true",num_str not_true),

 		(*"(~ True) = False"*)

 		Thm ("not_false",num_str not_false),

 		(*"(~ False) = True"*)

 		Thm ("and_true",and_true),

 		(*"(?a & True) = ?a"*)

 		Thm ("and_false",and_false),

 		(*"(?a & False) = False"*)

 		Thm ("or_true",or_true),

 		(*"(?a | True) = True"*)

 		Thm ("or_false",or_false),

 		(*"(?a | False) = ?a"*)

 		Thm ("rat_leq1",rat_leq1),

 		Thm ("rat_leq2",rat_leq2),

 		Thm ("rat_leq3",rat_leq3),

                 Thm ("refl",num_str refl),

 		Thm ("le_refl",num_str le_refl),

 		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

 		Calc ("op <",eval_equ "#less_"),

 		Calc ("op <=",eval_equ "#less_equal_"),

 		Calc ("Atools.ident",eval_ident "#ident_"),    

 		Calc ("Atools.is'_const",eval_const "#is_const_"),

 		Calc ("Atools.occurs'_in",eval_occurs_in ""),    

 		Calc ("Tools.matches",eval_matches "")

 		];

 val Atools_crls = 

     append_rls "Atools_crls" e_rls

                [Calc ("op =",eval_equal "#equal_"),

                 Thm ("not_true",num_str not_true),

 		Thm ("not_false",num_str not_false),

 		Thm ("and_true",and_true),

 		Thm ("and_false",and_false),

 		Thm ("or_true",or_true),

 		Thm ("or_false",or_false),

 		Thm ("rat_leq1",rat_leq1),

 		Thm ("rat_leq2",rat_leq2),

 		Thm ("rat_leq3",rat_leq3),

                 Thm ("refl",num_str refl),

 		Thm ("le_refl",num_str le_refl),

 		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

 		Calc ("op <",eval_equ "#less_"),

 		Calc ("op <=",eval_equ "#less_equal_"),

 		Calc ("Atools.ident",eval_ident "#ident_"),    

 		Calc ("Atools.is'_const",eval_const "#is_const_"),

 		Calc ("Atools.occurs'_in",eval_occurs_in ""),    

 		Calc ("Tools.matches",eval_matches "")

 		];

 (*val atools_erls = ... waere zu testen ...

     merge_rls calculate_Atools

 	      (append_rls Atools_erls (*i.A. zu viele rules*)

 			  [Calc ("Atools.ident",eval_ident "#ident_"),    

 			   Calc ("Atools.is'_const",eval_const "#is_const_"),

 			   Calc ("Atools.occurs'_in",

 				 eval_occurs_in "#occurs_in"),    

 			   Calc ("Tools.matches",eval_matches "#matches")

 			   ] (*i.A. zu viele rules*)

 			  );*)

 (* val atools_erls = prep_rls(

   Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), 

       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

       rules = [Thm ("refl",num_str refl),

 		Thm ("le_refl",num_str le_refl),

 		Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

 		Thm ("not_true",num_str not_true),

 		Thm ("not_false",num_str not_false),

 		Thm ("and_true",and_true),

 		Thm ("and_false",and_false),

 		Thm ("or_true",or_true),

 		Thm ("or_false",or_false),

 		Thm ("and_commute",num_str and_commute),

 		Thm ("or_commute",num_str or_commute),

 		Calc ("op <",eval_equ "#less_"),

 		Calc ("op <=",eval_equ "#less_equal_"),

 		Calc ("Atools.ident",eval_ident "#ident_"),    

 		Calc ("Atools.is'_const",eval_const "#is_const_"),

 		Calc ("Atools.occurs'_in",eval_occurs_in ""),    

 		Calc ("Tools.matches",eval_matches "")

 	       ],

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls);

 ruleset' := overwritelth thy 

 		(!ruleset',

 		 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)

 		  ]);

 *)

 "******* Atools.ML end *******";

 calclist':= overwritel (!calclist', 

    [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),

     ("some_occur_in",

      ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),

     ("is_atom"  ,("Atools.is'_atom",eval_is_atom "#is_atom_")),

     ("is_even"  ,("Atools.is'_even",eval_is_even "#is_even_")),

     ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),

     ("le"       ,("op <"        ,eval_equ "#less_")),

     ("leq"      ,("op <="       ,eval_equ "#less_equal_")),

     ("ident"    ,("Atools.ident",eval_ident "#ident_")),

     ("equal"    ,("op =",eval_equal "#equal_")),

     ("PLUS"     ,("op +"        ,eval_binop "#add_")),

     ("minus"    ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls

 	        			      no script with "minus"*)

     ("TIMES"    ,("op *"        ,eval_binop "#mult_")),

     ("DIVIDE"  ,("HOL.divide"  ,eval_cancel "#divide_")),

     ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),

     ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))

     ]);

 val list_rls = prep_rls(

     merge_rls "list_erls"

 	      (Rls {id="replaced",preconds = [], 

 		    rew_ord = ("termlessI", termlessI),

 		    erls = Rls {id="list_elrs", preconds = [], 

 				rew_ord = ("termlessI",termlessI), 

 				erls = e_rls, 

 				srls = Erls, calc = [], (*asm_thm = [],*)

 				rules = [Calc ("op +", eval_binop "#add_"),

 					 Calc ("op <",eval_equ "#less_")

 					 (*    ~~~~~~ for nth_Cons_*)

 					 ],

 				scr = EmptyScr},

 		    srls = Erls, calc = [], (*asm_thm = [], *)

 		    rules = [], scr = EmptyScr})

 	      list_rls);

 ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]);

 *}

 end