(* Title:  tools for arithmetic

    Author: Walther Neuper 010308

    (c) due to copyright terms

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 theory Atools imports Descript 

 uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")

 ("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")

 ("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")

 ("Interpret/inform.sml")("Interpret/mathengine.sml")

 ("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")

 ("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")

 ("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml")

 ("print_exn_G.sml")

 begin

 use "Interpret/mstools.sml"

 use "Interpret/ctree.sml"

 use "Interpret/ptyps.sml"    (*^^^ need files for: fun prep_pbt, fun store_pbt*)

 use "Interpret/generate.sml"

 use "Interpret/calchead.sml"

 use "Interpret/appl.sml"

 use "Interpret/rewtools.sml"

 use "Interpret/script.sml"

 use "Interpret/solve.sml"

 use "Interpret/inform.sml"       (*^^^ need files for: fun castab*)

 use "Interpret/mathengine.sml"

 use "xmlsrc/mathml.sml"

 use "xmlsrc/datatypes.sml"

 use "xmlsrc/pbl-met-hierarchy.sml"

 use "xmlsrc/thy-hierarchy.sml"   (*^^^ need files for: fun store_isa*)

 use "xmlsrc/interface-xml.sml"

 use "Frontend/messages.sml"

 use "Frontend/states.sml"    (*^^^ need files for: val states in Test_Isac.thy*)

 use "Frontend/interface.sml"

 use "print_exn_G.sml"

 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 FE-interface 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"

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

   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 /IsacKnowledge/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] TODO

 \item [*\_prls] 

 \item [*\_srls] 

 \end{description}

 {\tt append_rls, merge_rls, remove_rls} TODO

 *}

 ML {*

 val thy = @{theory};

 (** 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)) _ =

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

      tracing("@@@ 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"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

   ("TIMES"   ,("Groups.times_class.times"        ,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 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2

 		(*WN071229 "Rings.inverse_class.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 = "Groups.minus_class.minus" 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_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;

 > term2str t;

 val it = "-1 + 2 = 1"

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

 > val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" 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 ((*tracing"... 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) => 

 	    ((*tracing"... 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)))

 	     )

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

 		  NONE))

   | eval_equal _ _ _ _ = (tracing"... 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" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"))*)

 fun eval_cancel (thmid:string) "Rings.inverse_class.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

        | _ => ((*tracing"@@@ 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 = 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 ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

 		  $ su $ s'

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

 	    sum (Const ("Groups.plus_class.plus", [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 = Term_Ord.termless uv;

 fun term_ordI (_:subst) uv = Term_Ord.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 ("Groups.times_class.times",eval_binop "#mult_"),

 		Calc ("Groups.plus_class.plus", 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 @{thm if_True}),

 		Thm ("if_False",num_str @{thm 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 @{thm real_unari_minus}),

 		Calc ("Groups.plus_class.plus",eval_binop "#add_"),

 		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),

 		Calc ("Groups.times_class.times",eval_binop "#mult_")

 		];

 val Atools_erls = 

     append_rls "Atools_erls" e_rls

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

                 Thm ("not_true",num_str @{thm not_true}),

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

 		Thm ("not_false",num_str @{thm not_false}),

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

 		Thm ("and_true",num_str @{thm and_true}),

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

 		Thm ("and_false",num_str @{thm and_false}),

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

 		Thm ("or_true",num_str @{thm or_true}),

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

 		Thm ("or_false",num_str @{thm or_false}),

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

 		Thm ("rat_leq1",num_str @{thm rat_leq1}),

 		Thm ("rat_leq2",num_str @{thm rat_leq2}),

 		Thm ("rat_leq3",num_str @{thm rat_leq3}),

                 Thm ("refl",num_str @{thm refl}),

 		Thm ("real_le_refl",num_str @{thm real_le_refl}),

 		Thm ("radd_left_cancel_le",num_str @{thm 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 @{thm not_true}),

 		Thm ("not_false",num_str @{thm not_false}),

 		Thm ("and_true",num_str @{thm and_true}),

 		Thm ("and_false",num_str @{thm and_false}),

 		Thm ("or_true",num_str @{thm or_true}),

 		Thm ("or_false",num_str @{thm or_false}),

 		Thm ("rat_leq1",num_str @{thm rat_leq1}),

 		Thm ("rat_leq2",num_str @{thm rat_leq2}),

 		Thm ("rat_leq3",num_str @{thm rat_leq3}),

                 Thm ("refl",num_str @{thm refl}),

 		Thm ("real_le_refl",num_str @{thm real_le_refl}),

 		Thm ("radd_left_cancel_le",num_str @{thm 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 @{thm refl}),

 		Thm ("real_le_refl",num_str @{thm real_le_refl}),

 		Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),

 		Thm ("not_true",num_str @{thm not_true}),

 		Thm ("not_false",num_str @{thm not_false}),

 		Thm ("and_true",num_str @{thm and_true}),

 		Thm ("and_false",num_str @{thm and_false}),

 		Thm ("or_true",num_str @{thm or_true}),

 		Thm ("or_false",num_str @{thm or_false}),

 		Thm ("and_commute",num_str @{thm and_commute}),

 		Thm ("or_commute",num_str @{thm 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 @{theory})) 

       "empty_script")

       }:rls);

 ruleset' := overwritelth @{theory} 

 		(!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"     ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

     ("MINUS"    ,("Groups.minus_class.minus",eval_binop "#sub_")),

     ("TIMES"    ,("Groups.times_class.times"        ,eval_binop "#mult_")),

     ("DIVIDE"  ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),

     ("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 ("Groups.plus_class.plus", 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 @{theory} (!ruleset', [("list_rls", list_rls)]);

 *}

 end