(* WN.020812: theorems in the Reals,

   necessary for special rule sets, in addition to Isabelle2002.

   !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!

   !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   xxxI contain \<up> instead of ^ in the respective theorem xxx in 2002

   changed by: Richard Lang 020912

*)

theory Poly imports Simplify begin

subsection \<open>remark on term-structure of polynomials\<close>

text \<open>

WN190319:

the code below reflects missing coordination between two authors:

* ML: built the equation solver; simple rule-sets, programs; better predicates for specifications.

* MG: built simplification of polynomials with AC rewriting by ML code

WN020919:

*** there are 5 kinds of expanded normalforms ***

[1] 'complete polynomial' (Komplettes Polynom), univariate

   a_0 + a_1.x^1 +...+ a_n.x^n   not (a_n = 0)

	        not (a_n = 0), some a_i may be zero (DON'T disappear),

                variables in monomials lexicographically ordered and complete,

                x written as 1*x^1, ...

[2] 'polynomial' (Polynom), univariate and multivariate

   a_0 + a_1.x +...+ a_n.x^n   not (a_n = 0)

   a_0 + a_1.x_1.x_2^n_12...x_m^n_1m +...+  a_n.x_1^n.x_2^n_n2...x_m^n_nm

	        not (a_n = 0), some a_i may be zero (ie. monomials disappear),

                exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,

                and variables in monomials are lexicographically ordered  

   examples: [1]: "1 + (-10) * x \<up> 1 + 25 * x \<up> 2"

	     [1]: "11 + 0 * x \<up> 1 + 1 * x \<up> 2"

	     [2]: "x + (-50) * x \<up> 3"

	     [2]: "(-1) * x * y \<up> 2 + 7 * x \<up> 3"

[3] 'expanded_term' (Ausmultiplizierter Term):

   pull out unary minus to binary minus, 

   as frequently exercised in schools; other conditions for [2] hold however

   examples: "a \<up> 2 - 2 * a * b + b \<up> 2"

	     "4 * x \<up> 2 - 9 * y \<up> 2"

[4] 'polynomial_in' (Polynom in): 

   polynomial in 1 variable with arbitrary coefficients

   examples: "2 * x + (-50) * x \<up> 3"                     (poly in x)

	     "(u + v) + (2 * u \<up> 2) * a + (-u) * a \<up> 2 (poly in a)

[5] 'expanded_in' (Ausmultiplizierter Termin in): 

   analoguous to [3] with binary minus like [3]

   examples: "2 * x - 50 * x \<up> 3"                     (expanded in x)

	     "(u + v) + (2 * u \<up> 2) * a - u * a \<up> 2 (expanded in a)

\<close>

subsection \<open>consts definition for predicates in specifications\<close>

consts

  is_expanded_in :: "[real, real] => bool" ("_ is'_expanded'_in _") 

  is_poly_in     :: "[real, real] => bool" ("_ is'_poly'_in _")   (*RL DA *)

  has_degree_in  :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)

  is_polyrat_in  :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)

  is_multUnordered:: "real => bool" ("_ is'_multUnordered") 

  is_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)

  is_polyexp      :: "real => bool" ("_ is'_polyexp") 

subsection \<open>theorems not yet adopted from Isabelle\<close>

axiomatization where (*.not contained in Isabelle2002,

         stated as axioms, TODO: prove as theorems;

         theorem-IDs 'xxxI' with \<up> instead of ^ in 'xxx' in Isabelle2002.*)

  realpow_pow:             "(a \<up> b) \<up> c = a \<up> (b * c)" and

  realpow_addI:            "r \<up> (n + m) = r \<up> n * r \<up> m" and

  realpow_addI_assoc_l:    "r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s" and

  realpow_addI_assoc_r:    "s * r \<up> n * r \<up> m = s * r \<up> (n + m)" and

  realpow_oneI:            "r \<up> 1 = r" and

  realpow_zeroI:            "r \<up> 0 = 1" and

  realpow_eq_oneI:         "1 \<up> n = 1" and

  realpow_multI:           "(r * s) \<up> n = r \<up> n * s \<up> n"  and

  realpow_multI_poly:      "[| r is_polyexp; s is_polyexp |] ==>

			      (r * s) \<up> n = r \<up> n * s \<up> n"  and

  realpow_minus_oneI:      "(- 1) \<up> (2 * n) = 1"  and 

  real_diff_0:		         "0 - x = - (x::real)" and

  realpow_twoI:            "r \<up> 2 = r * r" and

  realpow_twoI_assoc_l:	  "r * (r * s) = r \<up> 2 * s" and

  realpow_twoI_assoc_r:	  "s * r * r = s * r \<up> 2" and

  realpow_two_atom:        "r is_atom ==> r * r = r \<up> 2" and

  realpow_plus_1:          "r * r \<up> n = r \<up> (n + 1)"   and       

  realpow_plus_1_assoc_l:  "r * (r \<up> m * s) = r \<up> (1 + m) * s"  and

  realpow_plus_1_assoc_l2: "r \<up> m * (r * s) = r \<up> (1 + m) * s"  and

  realpow_plus_1_assoc_r:  "s * r * r \<up> m = s * r \<up> (1 + m)" and

  realpow_plus_1_atom:     "r is_atom ==> r * r \<up> n = r \<up> (1 + n)" and

  realpow_def_atom:        "[| Not (r is_atom); 1 < n |]

			   ==> r \<up> n = r * r \<up> (n + -1)" and

  realpow_addI_atom:       "r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)" and

  realpow_minus_even:	     "n is_even ==> (- r) \<up> n = r \<up> n" and

  realpow_minus_odd:       "Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n" and

(* RL 020914 *)

  real_pp_binom_times:     "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and

  real_pm_binom_times:     "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and

  real_mp_binom_times:     "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and

  real_mm_binom_times:     "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and

  real_plus_binom_pow3:    "(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and

  real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==> 

			    (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and

  real_minus_binom_pow3:   "(a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3" and

  real_minus_binom_pow3_p: "(a + -1 * b) \<up> 3 = a \<up> 3 + -3*a \<up> 2*b + 3*a*b \<up> 2 +

                           -1*b \<up> 3" and

(* real_plus_binom_pow:        "[| n is_const;  3 < n |] ==>

			       (a + b) \<up> n = (a + b) * (a + b)\<up>(n - 1)" *)

  real_plus_binom_pow4:   "(a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)

                           *(a + b)" and

  real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==> 

			   (a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)

                           *(a + b)" and

  real_plus_binom_pow5:    "(a + b) \<up> 5 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)

                           *(a \<up> 2 + 2*a*b + b \<up> 2)" and

  real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==> 

			        (a + b) \<up> 5 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 

                                + b \<up> 3)*(a \<up> 2 + 2*a*b + b \<up> 2)" and

  real_diff_plus:          "a - b = a + -b" (*17.3.03: do_NOT_use*) and

  real_diff_minus:         "a - b = a + -1 * b" and

  real_plus_binom_times:   "(a + b)*(a + b) = a \<up> 2 + 2*a*b + b \<up> 2" and

  real_minus_binom_times:  "(a - b)*(a - b) = a \<up> 2 - 2*a*b + b \<up> 2" and

  (*WN071229 changed for Schaerding -----vvv*)

  (*real_plus_binom_pow2:  "(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)

  real_plus_binom_pow2:    "(a + b) \<up> 2 = (a + b) * (a + b)" and

  (*WN071229 changed for Schaerding -----\<up>*)

  real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>

			       (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and

  real_minus_binom_pow2:      "(a - b) \<up> 2 = a \<up> 2 - 2*a*b + b \<up> 2" and

  real_minus_binom_pow2_p:    "(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2" and

  real_plus_minus_binom1:     "(a + b)*(a - b) = a \<up> 2 - b \<up> 2" and

  real_plus_minus_binom1_p:   "(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2" and

  real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2" and

  real_plus_minus_binom2:     "(a - b)*(a + b) = a \<up> 2 - b \<up> 2" and

  real_plus_minus_binom2_p:   "(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and

  real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and

  real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2" and

  real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a \<up> 2 + -1*b \<up> 2" and

  real_num_collect:           "[| l is_const; m is_const |] ==>

			      l * n + m * n = (l + m) * n" and

(* FIXME.MG.0401: replace 'real_num_collect_assoc' 

	by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)

  real_num_collect_assoc:     "[| l is_const; m is_const |] ==> 

			      l * n + (m * n + k) = (l + m) * n + k" and

  real_num_collect_assoc_l:   "[| l is_const; m is_const |] ==>

			      l * n + (m * n + k) = (l + m)

				* n + k" and

  real_num_collect_assoc_r:   "[| l is_const; m is_const |] ==>

			      (k + m * n) + l * n = k + (l + m) * n" and

  real_one_collect:           "m is_const ==> n + m * n = (1 + m) * n" and

(* FIXME.MG.0401: replace 'real_one_collect_assoc' 

	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)

  real_one_collect_assoc:     "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and

  real_one_collect_assoc_l:   "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and

  real_one_collect_assoc_r:  "m is_const ==> (k + n) +  m * n = k + (1 + m) * n" and

(* FIXME.MG.0401: replace 'real_mult_2_assoc' 

	by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)

  real_mult_2_assoc:          "z1 + (z1 + k) = 2 * z1 + k" and

  real_mult_2_assoc_l:        "z1 + (z1 + k) = 2 * z1 + k" and

  real_mult_2_assoc_r:        "(k + z1) + z1 = k + 2 * z1" and

  real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and

  real_mult_minus1:       "-1 * z = - (z::real)" and

  real_mult_2:            "2 * z = z + (z::real)" and

  real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and

  real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"

subsection \<open>auxiliary functions\<close>

ML \<open>

val poly_consts =

  [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,

  \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,

  \<^const_name>\<open>powr\<close>];

\<close>

subsubsection \<open>for predicates in specifications (ML)\<close>

ML \<open>

(*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)

(*. a 'monomial t in variable v' is a term t with

  either (1) v NOT existent in t, or (2) v contained in t,

  if (1) then degree 0

  if (2) then v is a factor on the very right, ev. with exponent.*)

fun factor_right_deg (*case 2*)

	    (Const (\<^const_name>\<open>times\<close>, _) $ t1 $ (Const (\<^const_name>\<open>powr\<close>,_) $ vv $ Free (d, _))) v =

	   if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE

  | factor_right_deg (Const (\<^const_name>\<open>powr\<close>,_) $ vv $ Free (d,_)) v =

	   if (vv = v) then SOME (TermC.int_of_str d) else NONE

  | factor_right_deg (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ vv) v = 

	   if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE

  | factor_right_deg vv v =

	  if (vv = v) then SOME 1 else NONE;    

fun mono_deg_in m v =  (*case 1*)

	if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;

fun expand_deg_in t v =

	let

    fun edi ~1 ~1 (Const (\<^const_name>\<open>plus\<close>, _) $ t1 $ t2) =

          (case mono_deg_in t2 v of (* $ is left associative*)

            SOME d' => edi d' d' t1 | NONE => NONE)

      | edi ~1 ~1 (Const (\<^const_name>\<open>minus\<close>, _) $ t1 $ t2) =

          (case mono_deg_in t2 v of

            SOME d' => edi d' d' t1 | NONE => NONE)

      | edi d dmax (Const (\<^const_name>\<open>minus\<close>, _) $ t1 $ t2) =

          (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)

	        SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

          | NONE => NONE)

      | edi d dmax (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =

          (case mono_deg_in t2 v of

            SOME d' =>    (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)

              if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

          | NONE => NONE)

      | edi ~1 ~1 t =

          (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)

      | edi d dmax t = (*basecase last*)

    	    (case mono_deg_in t v of

    	      SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE

		      | NONE => NONE)

	in edi ~1 ~1 t end;

fun poly_deg_in t v =

	let

    fun edi ~1 ~1 (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =

		    (case mono_deg_in t2 v of (* $ is left associative *)

		      SOME d' => edi d' d' t1

        | NONE => NONE)

	    | edi d dmax (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =

		    (case mono_deg_in t2 v of

	        SOME d' =>    (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)

            if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

        | NONE => NONE)

	    | edi ~1 ~1 t =

        (case mono_deg_in t v of

		      d as SOME _ => d

        | NONE => NONE)

	    | edi d dmax t = (* basecase last *)

		    (case mono_deg_in t v of

		      SOME d' =>

            if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE

        | NONE => NONE)

	in edi ~1 ~1 t end;

\<close>

subsubsection \<open>for hard-coded AC rewriting (MG)\<close>

ML \<open>

(**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)

(*FIXME.0401: make SML-order local to make_polynomial(_) *)

(*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)

(* Polynom --> List von Monomen *) 

fun poly2list (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) = 

    (poly2list t1) @ (poly2list t2)

  | poly2list t = [t];

(* Monom --> Liste von Variablen *)

fun monom2list (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) = 

    (monom2list t1) @ (monom2list t2)

  | monom2list t = [t];

(* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)

fun get_basStr (Const (\<^const_name>\<open>powr\<close>,_) $ Free (str, _) $ _) = str

  | get_basStr (Free (str, _)) = str

  | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)

(*| get_basStr t = 

    raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)

(* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)

fun get_potStr (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free (str, _)) = str

  | get_potStr (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)

  | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)

  | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)

(*| get_potStr t = 

    raise ERROR("get_potStr: called with t= "^(UnparseC.term t));*)

(* Umgekehrte string_ord *)

val string_ord_rev =  rev_order o string_ord;

 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) 

    innerhalb eines Monomes:

    - zuerst lexikographisch nach Variablenname 

    - wenn gleich: nach steigender Potenz *)

fun var_ord (a,b: term) = prod_ord string_ord string_ord 

    ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));

(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen); 

   verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:

   - zuerst lexikographisch nach Variablenname 

   - wenn gleich: nach sinkender Potenz*)

fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev 

    ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));

(* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)

val sort_varList = sort var_ord;

(* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt 

   Argumente in eine Liste *)

fun args u : term list =

    let fun stripc (f$t, ts) = stripc (f, t::ts)

	  | stripc (t as Free _, ts) = (t::ts)

	  | stripc (_, ts) = ts

    in stripc (u, []) end;

(* liefert True, falls der Term (Liste von Termen) nur Zahlen 

   (keine Variablen) enthaelt *)

fun filter_num [] = true

  | filter_num [Free x] = if (TermC.is_num (Free x)) then true

				else false

  | filter_num ((Free _)::_) = false

  | filter_num ts =

    (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;

(* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt 

   dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)

fun is_nums t = filter_num [t];

(* Berechnet den Gesamtgrad eines Monoms *)

local 

    fun counter (n, []) = n

      | counter (n, x :: xs) = 

	if (is_nums x) then

	    counter (n, xs) 

	else 

	    (case x of 

		 (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ Free (str_h, T)) => 

		     if (is_nums (Free (str_h, T))) then

			 counter (n + (the (TermC.int_opt_of_string str_h)), xs)

		     else counter (n + 1000, xs) (*FIXME.MG?!*)

	       | (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _ ) => 

		     counter (n + 1000, xs) (*FIXME.MG?!*)

	       | (Free _) => counter (n + 1, xs)

	     (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)

	       | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)

in  

    fun monom_degree l = counter (0, l) 

end;(*local*)

(* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich 

   der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen, 

   werden jedoch dabei ignoriert (uebersprungen)  *)

fun dict_cond_ord _ _ ([], []) = EQUAL

  | dict_cond_ord _ _ ([], _ :: _) = LESS

  | dict_cond_ord _ _ (_ :: _, []) = GREATER

  | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =

    (case (cond x, cond y) of 

	 (false, false) => (case elem_ord (x, y) of 

				EQUAL => dict_cond_ord elem_ord cond (xs, ys) 

			      | ord => ord)

       | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)

       | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)

       | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys) );

(* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):

   zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen - 

   dabei werden Koeffizienten ignoriert (2*3*a \<up> 2*4*b gilt wie a \<up> 2*b) *)

fun degree_ord (xs, ys) =

	    prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums) 

	    ((monom_degree xs, xs), (monom_degree ys, ys));

fun hd_str str = substring (str, 0, 1);

fun tl_str str = substring (str, 1, (size str) - 1);

(* liefert nummerischen Koeffizienten eines Monoms oder NONE *)

fun get_koeff_of_mon [] =  raise ERROR("get_koeff_of_mon: called with l = []")

  | get_koeff_of_mon (x::_) = if is_nums x then SOME x else NONE;

(* wandelt Koeffizient in (zum sortieren geeigneten) String um *)

fun koeff2ordStr (SOME x) = (case x of 

				 (Free (str, _)) => 

				     if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)

				     else str

			       | _ => "aaa") (* "num.Ausdruck" --> gross *)

  | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)

(* Order zum Vergleich von Koeffizienten (strings): 

   "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)

fun compare_koeff_ord (xs, ys) = 

    string_ord ((koeff2ordStr o get_koeff_of_mon) xs,

		(koeff2ordStr o get_koeff_of_mon) ys);

(* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)

fun koeff_degree_ord (xs, ys) =

	    prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));

(* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels 

   Gesamtgradordnung *)

val sort_monList = sort koeff_degree_ord;

(* Alternativ zu degree_ord koennte auch die viel einfachere und 

   kuerzere Ordnung simple_ord verwendet werden - ist aber nicht 

   fuer unsere Zwecke geeignet!

fun simple_ord (al,bl: term list) = dict_ord string_ord 

	 (map get_basStr al, map get_basStr bl); 

val sort_monList = sort simple_ord; *)

(* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt 

   (mit gewuenschtem Typen T) *)

fun plus T = Const (\<^const_name>\<open>plus\<close>, [T,T] ---> T);

fun mult T = Const (\<^const_name>\<open>times\<close>, [T,T] ---> T);

fun binop op_ t1 t2 = op_ $ t1 $ t2;

fun create_prod T (a,b) = binop (mult T) a b;

fun create_sum T (a,b) = binop (plus T) a b;

(* löscht letztes Element einer Liste *)

fun drop_last l = take ((length l)-1,l);

(* Liste von Variablen --> Monom *)

fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);

(* Bemerkung: 

   foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei 

   gleiche Monome zusammengefasst werden können (collect_numerals)! 

   zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)

(* Liste von Monomen --> Polynom *)	

fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);

(* Bemerkung: 

   foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) - 

   bessere Darstellung, da keine Klammern sichtbar! 

   (und discard_parentheses in make_polynomial hat weniger zu tun) *)

(* sorts the variables (faktors) of an expanded polynomial lexicographical *)

fun sort_variables t = 

    let

	val ll =  map monom2list (poly2list t);

	val lls = map sort_varList ll; 

	val T = type_of t;

	val ls = map (create_monom T) lls;

    in create_polynom T ls end;

(* sorts the monoms of an expanded and variable-sorted polynomial 

   by total_degree *)

fun sort_monoms t = 

    let

	val ll =  map monom2list (poly2list t);

	val lls = sort_monList ll;

	val T = type_of t;

	val ls = map (create_monom T) lls;

    in create_polynom T ls end;

\<close>

subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>

ML \<open>

local (*. for make_polynomial .*)

open Term;  (* for type order = EQUAL | LESS | GREATER *)

fun pr_ord EQUAL = "EQUAL"

  | pr_ord LESS  = "LESS"

  | pr_ord GREATER = "GREATER";

fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)

  (case a of

     \<^const_name>\<open>powr\<close> => ((("|||||||||||||", 0), T), 0)    (*WN greatest string*)

   | _ => (((a, 0), T), 0))

  | dest_hd' (Free (a, T)) = (((a, 0), T), 1)

  | dest_hd' (Var v) = (v, 2)

  | dest_hd' (Bound i) = ((("", i), dummyT), 3)

  | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)

  | dest_hd' t = raise TERM ("dest_hd'", [t]);

fun size_of_term' (Const(str,_) $ t) =

  if \<^const_name>\<open>powr\<close>= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)

  | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body

  | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t

  | size_of_term' _ = 1;

fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

    (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)

  | term_ord' pr thy (t, u) =

    (if pr then 

	   let

       val (f, ts) = strip_comb t and (g, us) = strip_comb u;

       val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^

         commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");

       val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^

         commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");

       val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^

         string_of_int (size_of_term' u) ^ ")");

       val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o hd_ord) (f,g));

       val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));

       val _ = tracing ("-------");

     in () end

       else ();

	 case int_ord (size_of_term' t, size_of_term' u) of

	   EQUAL =>

	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in

	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 

	     | ord => ord)

	     end

	 | ord => ord)

and hd_ord (f, g) =                                        (* ~ term.ML *)

  prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)

and terms_ord _ pr (ts, us) = 

    list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);

in

fun ord_make_polynomial (pr:bool) thy (_: subst) tu = 

    (term_ord' pr thy(***) tu = LESS );

end;(*local*)

Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)

[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]);

\<close>

subsection \<open>predicates\<close>

subsubsection \<open>in specifications\<close>

ML \<open>

(* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)

fun is_polyrat_in t v = 

  let

   	fun finddivide (_ $ _ $ _ $ _) _ = raise ERROR("is_polyrat_in:")

	    (* at the moment there is no term like this, but ....*)

	  | finddivide (Const (\<^const_name>\<open>divide\<close>,_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)

	  | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v

	  | finddivide (_ $ t1) v = finddivide t1 v

	  | finddivide _ _ = false;

  in finddivide t v end;

fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;

fun is_poly_in t v =     case poly_deg_in t v of SOME _ => true | NONE => false;

fun has_degree_in t v =  case expand_deg_in t v of SOME d => d | NONE => ~1;

(*.the expression contains + - * ^ only ?

   this is weaker than 'is_polynomial' !.*)

fun is_polyexp (Free _) = true

  | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)

  | is_polyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true

  | is_polyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true

  | is_polyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true

  | is_polyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true

  | is_polyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const (\<^const_name>\<open>minus\<close>,_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp _ = false;

\<close>

subsubsection \<open>for hard-coded AC rewriting\<close>

ML \<open>

(* auch Klammerung muss übereinstimmen;

   sort_variables klammert Produkte rechtslastig*)

fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));

fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));

\<close>

subsection \<open>evaluations functions\<close>

subsubsection \<open>for predicates\<close>

ML \<open>

fun eval_is_polyrat_in _ _(p as (Const ("Poly.is_polyrat_in",_) $ t $ v)) _  =

    if is_polyrat_in t v 

    then SOME ((UnparseC.term p) ^ " = True",

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

    else SOME ((UnparseC.term p) ^ " = True",

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

  | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);

(*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)

fun eval_is_expanded_in _ _ 

       (p as (Const ("Poly.is_expanded_in",_) $ t $ v)) _ =

    if is_expanded_in t v

    then SOME ((UnparseC.term p) ^ " = True",

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

    else SOME ((UnparseC.term p) ^ " = True",

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

  | eval_is_expanded_in _ _ _ _ = NONE;

(*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)

fun eval_is_poly_in _ _ 

       (p as (Const ("Poly.is_poly_in",_) $ t $ v)) _ =

    if is_poly_in t v

    then SOME ((UnparseC.term p) ^ " = True",

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

    else SOME ((UnparseC.term p) ^ " = True",

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

  | eval_is_poly_in _ _ _ _ = NONE;

(*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)

fun eval_has_degree_in _ _ 

	     (p as (Const ("Poly.has_degree_in",_) $ t $ v)) _ =

    let val d = has_degree_in t v

	val d' = TermC.term_of_num HOLogic.realT d

    in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),

	      HOLogic.Trueprop $ (TermC.mk_equality (p, d')))

    end

  | eval_has_degree_in _ _ _ _ = NONE;

(*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)

fun eval_is_polyexp (thmid:string) _ 

		       (t as (Const("Poly.is_polyexp", _) $ arg)) thy = 

    if is_polyexp arg

    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

  | eval_is_polyexp _ _ _ _ = NONE; 

\<close>

subsubsection \<open>for hard-coded AC rewriting\<close>

ML \<open>

(*WN.18.6.03 *)

(*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)

fun eval_is_addUnordered (thmid:string) _ 

		       (t as (Const("Poly.is_addUnordered", _) $ arg)) thy = 

    if is_addUnordered arg

    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

  | eval_is_addUnordered _ _ _ _ = NONE; 

fun eval_is_multUnordered (thmid:string) _ 

		       (t as (Const("Poly.is_multUnordered", _) $ arg)) thy = 

    if is_multUnordered arg

    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 

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

  | eval_is_multUnordered _ _ _ _ = NONE; 

\<close>

calculation is_polyrat_in = \<open>eval_is_polyrat_in "#eval_is_polyrat_in"\<close>

calculation is_expanded_in = \<open>eval_is_expanded_in ""\<close>

calculation is_poly_in = \<open>eval_is_poly_in ""\<close>

calculation has_degree_in = \<open>eval_has_degree_in ""\<close>

calculation is_polyexp = \<open>eval_is_polyexp ""\<close>

calculation is_multUnordered = \<open>eval_is_multUnordered ""\<close>

calculation is_addUnordered = \<open>eval_is_addUnordered ""\<close>

subsection \<open>rule-sets\<close>

subsubsection \<open>without specific order\<close>

ML \<open>

(* used only for merge *)

val calculate_Poly = Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];

(*.for evaluation of conditions in rewrite rules.*)

val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls

  [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),

  \<^rule_thm>\<open>real_unari_minus\<close>,

  \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),

  \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),

  \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),

  \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];

val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls

  [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),

  \<^rule_thm>\<open>real_unari_minus\<close>,

  \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),

  \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),

  \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),

  \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];

\<close>

ML \<open>

val expand =

  Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],

      rules = [\<^rule_thm>\<open>distrib_right\<close>,

	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	       \<^rule_thm>\<open>distrib_left\<close>

	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	       ], scr = Rule.Empty_Prog};

val discard_minus =

  Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

      rules =

       [\<^rule_thm>\<open>real_diff_minus\<close>,

          (*"a - b = a + -1 * b"*)

	        \<^rule_thm_sym>\<open>real_mult_minus1\<close>

	          (*- ?z = "-1 * ?z"*)],

	      scr = Rule.Empty_Prog};

val expand_poly_ = 

  Rule_Def.Repeat{id = "expand_poly_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules =

        [\<^rule_thm>\<open>real_plus_binom_pow4\<close>,

	           (*"(a + b) \<up> 4 = ... "*)

	         \<^rule_thm>\<open>real_plus_binom_pow5\<close>,

	           (*"(a + b) \<up> 5 = ... "*)

	         \<^rule_thm>\<open>real_plus_binom_pow3\<close>,

	           (*"(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)

	         (*WN071229 changed/removed for Schaerding -----vvv*)

	         (*\<^rule_thm>\<open>real_plus_binom_pow2\<close>,*)

	           (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)

	         \<^rule_thm>\<open>real_plus_binom_pow2\<close>,

	           (*"(a + b) \<up> 2 = (a + b) * (a + b)"*)

	         (*\<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>,*)

	           (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)

	         (*\<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,*)

	           (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)

	         (*WN071229 changed/removed for Schaerding -----\<up>*)

	         \<^rule_thm>\<open>distrib_right\<close>,

	           (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	         \<^rule_thm>\<open>distrib_left\<close>,

	           (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	         \<^rule_thm>\<open>realpow_multI\<close>,

	           (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)

	         \<^rule_thm>\<open>realpow_pow\<close>

	           (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)

	       ], scr = Rule.Empty_Prog};

val expand_poly_rat_ = 

  Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls =  Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty

	        [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")

		 ],

      srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = 

        [\<^rule_thm>\<open>real_plus_binom_pow4_poly\<close>,

	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 4 = ... "*)

	 \<^rule_thm>\<open>real_plus_binom_pow5_poly\<close>,

	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 5 = ... "*)

	 \<^rule_thm>\<open>real_plus_binom_pow2_poly\<close>,

	     (*"[| a is_polyexp; b is_polyexp |] ==>

		            (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)

	 \<^rule_thm>\<open>real_plus_binom_pow3_poly\<close>,

	     (*"[| a is_polyexp; b is_polyexp |] ==> 

			(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)

	 \<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>,

	     (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)

	 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,

	     (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)

	 \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>,

	       (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	 \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>,

	     (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	 \<^rule_thm>\<open>realpow_multI_poly\<close>,

	     (*"[| r is_polyexp; s is_polyexp |] ==> 

		            (r * s) \<up> n = r \<up> n * s \<up> n"*)

	  \<^rule_thm>\<open>realpow_pow\<close>

	      (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)

	 ], scr = Rule.Empty_Prog};

val simplify_power_ = 

  Rule_Def.Repeat{id = "simplify_power_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty, srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen

		a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)

	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,	

	       (*"r * r = r \<up> 2"*)

	       \<^rule_thm>\<open>realpow_twoI_assoc_l\<close>,

	       (*"r * (r * s) = r \<up> 2 * s"*)

	       \<^rule_thm>\<open>realpow_plus_1\<close>,		

	       (*"r * r \<up> n = r \<up> (n + 1)"*)

	       \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>,

	       (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)

	       (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)

	       \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>,

	       (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)

	       \<^rule_thm_sym>\<open>realpow_addI\<close>,

	       (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)

	       \<^rule_thm>\<open>realpow_addI_assoc_l\<close>,

	       (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)

	       (* ist in expand_poly - wird hier aber auch gebraucht, wegen: 

		  "r * r = r \<up> 2" wenn r=a \<up> b*)

	       \<^rule_thm>\<open>realpow_pow\<close>

	       (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)

	       ], scr = Rule.Empty_Prog};

val calc_add_mult_pow_ = 

  Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,

      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 

	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),

	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))

	      ],

      errpatts = [],

      rules = [\<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),

	       \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),

	       \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")

	       ], scr = Rule.Empty_Prog};

val reduce_012_mult_ = 

  Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)

               \<^rule_thm>\<open>mult_1_right\<close>,

	       (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*) 

	       \<^rule_thm>\<open>realpow_zeroI\<close>,

	       (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*)

	       \<^rule_thm>\<open>realpow_oneI\<close>,

	       (*"r \<up> 1 = r"*)

	       \<^rule_thm>\<open>realpow_eq_oneI\<close>

	       (*"1 \<up> n = 1"*)

	       ], scr = Rule.Empty_Prog};

val collect_numerals_ = 

  Rule_Def.Repeat{id = "collect_numerals_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Atools_erls, srls = Rule_Set.Empty,

      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))

	      ], errpatts = [],

      rules = 

        [\<^rule_thm>\<open>real_num_collect\<close>, 

	     (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)

	 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,

	     (*"[| l is_const; m is_const |] ==>  \

					\(k + m * n) + l * n = k + (l + m)*n"*)

	 \<^rule_thm>\<open>real_one_collect\<close>,	

	     (*"m is_const ==> n + m * n = (1 + m) * n"*)

	 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, 

	     (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)

         \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),

	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen

		     (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)

         \<^rule_thm>\<open>real_mult_2_assoc_r\<close>,

	     (*"(k + z1) + z1 = k + 2 * z1"*)

	 \<^rule_thm_sym>\<open>real_mult_2\<close>

	     (*"z1 + z1 = 2 * z1"*)

	], scr = Rule.Empty_Prog};

val reduce_012_ = 

  Rule_Def.Repeat{id = "reduce_012_", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],

      rules = [\<^rule_thm>\<open>mult_1_left\<close>,                 

	       (*"1 * z = z"*)

	       \<^rule_thm>\<open>mult_zero_left\<close>,        

	       (*"0 * z = 0"*)

	       \<^rule_thm>\<open>mult_zero_right\<close>,

	       (*"z * 0 = 0"*)

	       \<^rule_thm>\<open>add_0_left\<close>,

	       (*"0 + z = z"*)

	       \<^rule_thm>\<open>add_0_right\<close>,

	       (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)

	       (*\<^rule_thm>\<open>realpow_oneI\<close>*)

	       (*"?r \<up> 1 = ?r"*)

	       \<^rule_thm>\<open>division_ring_divide_zero\<close>

	       (*"0 / ?x = 0"*)

	       ], scr = Rule.Empty_Prog};

val discard_parentheses1 = 

    Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty 

	       [\<^rule_thm_sym>\<open>mult.assoc\<close>

		(*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)

		(*\<^rule_thm_sym>\<open>add.assoc\<close>*)

		(*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)

		 ];

val expand_poly =

  Rule_Def.Repeat{id = "expand_poly", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      (*asm_thm = [],*)

      rules = [\<^rule_thm>\<open>distrib_right\<close>,

	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	       \<^rule_thm>\<open>distrib_left\<close>,

	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	       (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),

		....... 18.3.03 undefined???*)

	       \<^rule_thm>\<open>real_plus_binom_pow2\<close>,

	       (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)

	       \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>,

	       (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)

	       \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>,

	       (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)

	       \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>,

	       (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)

	       \<^rule_thm>\<open>minus_minus\<close>,

	       (*"- (- ?z) = ?z"*)

	       \<^rule_thm>\<open>real_diff_minus\<close>,

	       (*"a - b = a + -1 * b"*)

	       \<^rule_thm_sym>\<open>real_mult_minus1\<close>

	       (*- ?z = "-1 * ?z"*)

	       (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)

	       (*"- (?x + ?y) = - ?x + - ?y"*)

	       (*\<^rule_thm>\<open>real_diff_plus\<close>*)

	       (*"a - b = a + -b"*)

	       ], scr = Rule.Empty_Prog};

val simplify_power = 

  Rule_Def.Repeat{id = "simplify_power", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty, srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = [\<^rule_thm>\<open>realpow_multI\<close>,

	       (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)

	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,	

	       (*"r1 * r1 = r1 \<up> 2"*)

	       \<^rule_thm>\<open>realpow_plus_1\<close>,		

	       (*"r * r \<up> n = r \<up> (n + 1)"*)

	       \<^rule_thm>\<open>realpow_pow\<close>,

	       (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)

	       \<^rule_thm_sym>\<open>realpow_addI\<close>,

	       (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)

	       \<^rule_thm>\<open>realpow_oneI\<close>,

	       (*"r \<up> 1 = r"*)

	       \<^rule_thm>\<open>realpow_eq_oneI\<close>

	       (*"1 \<up> n = 1"*)

	       ], scr = Rule.Empty_Prog};

val collect_numerals = 

  Rule_Def.Repeat{id = "collect_numerals", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,

      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 

	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),

	      ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))

	      ], errpatts = [],

      rules = [\<^rule_thm>\<open>real_num_collect\<close>, 

	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)

	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,

	       (*"[| l is_const; m is_const |] ==>  

				l * n + (m * n + k) =  (l + m) * n + k"*)

	       \<^rule_thm>\<open>real_one_collect\<close>,	

	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 

	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

	       \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 

	       \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),

	       \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")

	       ], scr = Rule.Empty_Prog};

val reduce_012 = 

  Rule_Def.Repeat{id = "reduce_012", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

      erls = Rule_Set.empty,srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = [\<^rule_thm>\<open>mult_1_left\<close>,                 

	       (*"1 * z = z"*)

	       (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)

	       (*"-1 * z = - z"*)

	       Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),

	       (*- (?x * ?y) = "- ?x * ?y"*)

	       (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,

	       (*"- ?x * - ?y = ?x * ?y"*)---*)

	       \<^rule_thm>\<open>mult_zero_left\<close>,        

	       (*"0 * z = 0"*)

	       \<^rule_thm>\<open>add_0_left\<close>,

	       (*"0 + z = z"*)

	       \<^rule_thm>\<open>right_minus\<close>,

	       (*"?z + - ?z = 0"*)

	       \<^rule_thm_sym>\<open>real_mult_2\<close>,	

	       (*"z1 + z1 = 2 * z1"*)

	       \<^rule_thm>\<open>real_mult_2_assoc\<close>

	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

	       ], scr = Rule.Empty_Prog};

val discard_parentheses = 

    Rule_Set.append_rules "discard_parentheses" Rule_Set.empty 

	       [\<^rule_thm_sym>\<open>mult.assoc\<close>,	\<^rule_thm_sym>\<open>add.assoc\<close>];

\<close>

subsubsection \<open>hard-coded AC rewriting\<close>

ML \<open>

(*MG.0401: termorders for multivariate polys dropped due to principal problems:

  (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)

val order_add_mult = 

  Rule_Def.Repeat{id = "order_add_mult", preconds = [], 

      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),

      erls = Rule_Set.empty,srls = Rule_Set.Empty,

      calc = [], errpatts = [],

      rules = [\<^rule_thm>\<open>mult.commute\<close>,

	       (* z * w = w * z *)