(* Title:  tools for arithmetic

   Author: Walther Neuper 010308

   (c) due to copyright terms

*)

theory Atools imports Descript Script

begin

subsection \<open>preparation to build up a program from rules\<close>

partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"

  where "auto_generated t_t = t_t"

partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"

  where "auto_generated_inst t_t v =  t_t"

subsection \<open>use preparation\<close>

ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"

subsection \<open>consts & axiomatization\<close>

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"

  lastI            :: "'a list \<Rightarrow> 'a"

axiomatization where (*for evaluating the assumptions of conditional rules*)

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

  real_unari_minus:   "- a = (-1) * a" and

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

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

  not_true:           "(~ True) = False" and

  not_false:          "(~ False) = True"

axiomatization where (*..if replaced by "and" we get error:

Type unification failed: No type arity bool :: zero ...*)

  and_true:           "(a & True) = a" and

  and_false:          "(a & False) = False" and

  or_true:            "(a | True) = True" and

  or_false:           "(a | False) = a" and

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

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

axiomatization where (*..if replaced by "and" we get error:

Type unification failed: No type arity bool :: zero ...*)

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

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

  rat_leq2:	      "d ~= 0 ==>

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

  rat_leq3:	      "b ~= 0 ==>

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

subsection \<open>Coding standards\<close>

text \<open>copy from doc/math-eng.tex WN.28.3.03

WN071228 extended\<close>

subsubsection \<open>Identifiers\<close>

text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).

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

subsubsection \<open>Rule sets\<close>

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

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 {\tt Theory_Data} (KEStore_Elems.add_rlss,

KEStore_Elems.get_rlss). 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 Rule.append_rls, Rule.merge_rls, remove_rls} TODO

\<close>

subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>

ML \<open>

val thy = @{theory};

fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);

(*("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= "^(Rule.term2str v));

     tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)

     if occurs_in v t

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

	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

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

	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))

  | 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 (TermC.isalist2list vs) t

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

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

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

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | 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 (TermC.mk_thmid thmid n "", 

			      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

       | _ => SOME (TermC.mk_thmid thmid "" "", 

		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

  | 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 TermC.int_of_str_opt n of

	      SOME i =>

	      if even i then SOME (TermC.mk_thmid thmid n "", 

				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

	      else SOME (TermC.mk_thmid thmid "" "", 

			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

	    | _ => 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 (TermC.mk_thmid thmid n1 "", 

	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

     | Free (n1,_) =>

	 if TermC.is_num' n1

	   then SOME (TermC.mk_thmid thmid n1 "", 

		      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

	 else SOME (TermC.mk_thmid thmid n1 "", 

		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

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

       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 

	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

     | _ => (*NONE*)

       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 

		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

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

  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 TermC.int_of_str_opt str of

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

       | NONE => NONE)

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

		   (Const ("Product_Type.Pair", _) $

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

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

    (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

	(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', _) $ v $ t1) $ t2)) _ =  (* binary . (v.n1).n2 *)

    if op0 = op0' then

      case (numeral t1, numeral t2) of

        (SOME n1, SOME n2) =>

          let 

            val (T1, _, _) = TermC.dest_binop_typ t0

            val res = 

              calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2

              (*WN071229 "Rings.divide_class.divide" never tried*)

            val rhs = var_op_float v op_ t0 T1 res

            val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

          in SOME ("#: " ^ Rule.term2str prop, prop) end

      | _ => NONE

    else NONE

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

      (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =  (* 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, _, _) = TermC.dest_binop_typ t0

            val res = calcul op0 n1 n2

            val rhs = float_op_var v op_ t0 T1 res

            val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

          in SOME ("#: " ^ Rule.term2str prop, prop) end

      | _ => NONE

    else NONE

  | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ =   (* binary . n1.n2 *)

    (case (numeral t1, numeral t2) of

      (SOME n1, SOME n2) =>

        let 

          val (_, _, Trange) = TermC.dest_binop_typ t0;

          val res = calcul op0 n1 n2;

          val rhs = term_of_float Trange res;

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

        in SOME ("#: " ^ Rule.term2str prop, prop) end

    | _ => NONE)

  | eval_binop _ _ _ _ = NONE; 

(*

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

> Rule.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;

> Rule.term2str t;

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

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

(*("le"      ,("Orderings.ord_class.less"        ,eval_equ "#less_")),

  ("leq"     ,("Orderings.ord_class.less_eq"       ,eval_equ "#less_equal_"))*)

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

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

    (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

	 (SOME n1', SOME n2') =>

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

    then SOME (TermC.mk_thmid thmid n1 n2, 

	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else SOME (TermC.mk_thmid thmid n1 n2,  

	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

       | _ => NONE)

  | eval_equ _ _ _ _ = NONE;

(*evaluate identity

> reflI;

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

> val t = str2term "x = 0";

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

> val t = str2term "1 = 0";

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

----------- thus needs Rule.Calc !

> val t = str2term "0 = 0";

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

> Rule.term2str t';

val it = "HOL.True"

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

atomt t; Rule.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 (TermC.mk_thmid thmid 

	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"), 

	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else SOME (TermC.mk_thmid thmid  

	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),  

	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

  | eval_ident _ _ _ _ = NONE;

(* TODO

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

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

> Rule.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;

> Rule.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;

> Rule.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"   ,("HOL.eq",eval_equal "#equal_")):calc*)

fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy = 

  if t1 = t2

  then SOME (TermC.mk_thmid thmid 

                ("(" ^ Rule.term_to_string''' thy t1 ^ ")")

                ("(" ^ Rule.term_to_string''' thy t2 ^ ")"), 

       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else (case (TermC.is_atom t1, TermC.is_atom t2) of

      (true, true) => 

      SOME (TermC.mk_thmid thmid  

         ("(" ^ Rule.term_to_string''' thy t1 ^ ")")

         ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),

      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

    | _ => NONE)                             (* NOT is_atom t1,t2 --> rew_sub *)

  | eval_equal _ _ _ _ = NONE;                                  (* error-exit *)

(*

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;

> Rule.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;

> Rule.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;

> Rule.term2str t';

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

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

*)

\<close>

subsection \<open>evaluation on the meta-level\<close>

ML \<open>

(*. evaluate HOL.divide .*)

(*("DIVIDE" ,("Rings.divide_class.divide"  ,eval_cancel "#divide_e"))*)

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

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

    (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

	 (SOME n1', SOME n2') =>

  let 

    val sg = Calc.sign_mult n1' n2';

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

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

  in if gcd' = abs n2' 

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

	      val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

	  in SOME (TermC.mk_thmid thmid n1 n2, prop) end     

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

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

				   ((abs n2') div gcd')

	      val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

	  in SOME (TermC.mk_thmid thmid 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 (Rule.term2str t ^ " = " ^ Rule.term2str arg,

	       HOLogic.Trueprop $ (TermC.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 ("HOL.eq", _) $ (f2 $ _) $ _)) _ =

    if f1 = f2 

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

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

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

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

| 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 ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2

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

				   ^Rule.term2str f1^") ("^Rule.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' = ((TermC.list2isalist HOLogic.boolT) o 

		   (filter (same_funid fid))) (TermC.isalist2list fs)

    in SOME (Rule.term2str (TermC.mk_equality (p, fs')),

	       HOLogic.Trueprop $ (TermC.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 = TermC.isalist2list l

	val lhss = map Tools.lhs isal

	val sum = list2sum lhss

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

	  HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))

    end

| eval_boollist2sum _ _ _ _ = NONE;

\<close>

subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>

ML \<open>

local

open Term;

in

fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;

fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;

end;

val list_rls = Rule.append_rls "list_rls" list_rls

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

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

		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

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

		Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)

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

		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),

		Rule.Thm ("if_False",TermC.num_str @{thm if_False})

		];

\<close>

ML \<open>

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

val tless_true = Rule.dummy_ord;

Rule.rew_ord' := overwritel (! Rule.rew_ord',

			[("tless_true", tless_true),

			 ("e_rew_ord'", tless_true),

			 ("dummy_ord", Rule.dummy_ord)]);

val calculate_Base_Tools = 

    Rule.append_rls "calculate_Atools" Rule.e_rls

               [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

		Rule.Calc ("HOL.eq",eval_equal "#equal_"),

		Rule.Thm  ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),

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

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

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

		];

\<close>

find_theorems (9) "?n <= ?n"

ML \<open>

val Atools_erls = 

    Rule.append_rls "Atools_erls" Rule.e_rls

               [Rule.Calc ("HOL.eq",eval_equal "#equal_"),

                Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

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

		Rule.Thm ("not_false",TermC.num_str @{thm not_false}),

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

		Rule.Thm ("and_true",TermC.num_str @{thm and_true}),

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

		Rule.Thm ("and_false",TermC.num_str @{thm and_false}),

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

		Rule.Thm ("or_true",TermC.num_str @{thm or_true}),

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

		Rule.Thm ("or_false",TermC.num_str @{thm or_false}),

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

		Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),

		Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),

		Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),

                Rule.Thm ("refl",TermC.num_str @{thm refl}),

		Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),

		Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),

		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

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

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

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

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

		];

\<close>

ML \<open>

val Atools_crls = 

    Rule.append_rls "Atools_crls" Rule.e_rls

               [Rule.Calc ("HOL.eq",eval_equal "#equal_"),

                Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

		Rule.Thm ("not_false",TermC.num_str @{thm not_false}),

		Rule.Thm ("and_true",TermC.num_str @{thm and_true}),

		Rule.Thm ("and_false",TermC.num_str @{thm and_false}),

		Rule.Thm ("or_true",TermC.num_str @{thm or_true}),

		Rule.Thm ("or_false",TermC.num_str @{thm or_false}),

		Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),

		Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),

		Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),

                Rule.Thm ("refl",TermC.num_str @{thm refl}),

		Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),

		Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),

		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

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

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

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

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

		];

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

    Rule.merge_rls calculate_Atools

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

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

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

			   Rule.Calc ("Atools.occurs'_in",

				 eval_occurs_in "#occurs_in"),    

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

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

			  );*)

(* val atools_erls = prep_rls'(     (*outcommented*)

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

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Thm ("refl",num_str @{thm refl}),

		Rule.Thm ("order_refl",num_str @{thm order_refl}),

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

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

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

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

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

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

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

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

		Rule.Thm ("or_commute",num_str @{thm or_commute}),

		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

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

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

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

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

	       ],

      scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")

      });

*)

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

\<close>

subsection \<open>write to KEStore: calcs, rule-sets\<close>

setup \<open>KEStore_Elems.add_calcs

  [("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"       ,("Orderings.ord_class.less", eval_equ "#less_")),

    ("leq"      ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),

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

    ("equal"    ,("HOL.eq", 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.divide_class.divide", eval_cancel "#divide_e")),

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

    ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))]\<close>

ML \<open>

val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"

	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),

    erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),

        Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")

        (*    ~~~~~~ for nth_Cons_*)],

      scr = Rule.EmptyScr},

    srls = Rule.Erls, calc = [], errpatts = [],

    rules = [], scr = Rule.EmptyScr})

  list_rls);

\<close>

setup \<open>KEStore_Elems.add_rlss

  [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>

ML \<open>

\<close> ML \<open>

\<close> 

end