(* 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 ^^^ instead of ^ in the respective theorem xxx in 2002

   changed by: Richard Lang 020912

*)

theory Poly imports Simplify begin

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

  Expand'_binoms

             :: "['y, 

		    'y] => 'y"

               ("((Script Expand'_binoms (_ =))// 

                    (_))" 9)

(*-------------------- rules------------------------------------------------*)

axioms (*.not contained in Isabelle2002,

         stated as axioms, TODO: prove as theorems;

         theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)

  realpow_pow:             "(a ^^^ b) ^^^ c = a ^^^ (b * c)"

  realpow_addI:            "r ^^^ (n + m) = r ^^^ n * r ^^^ m"

  realpow_addI_assoc_l:    "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"

  realpow_addI_assoc_r:    "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"

  realpow_oneI:            "r ^^^ 1 = r"

  realpow_zeroI:            "r ^^^ 0 = 1"

  realpow_eq_oneI:         "1 ^^^ n = 1"

  realpow_multI:           "(r * s) ^^^ n = r ^^^ n * s ^^^ n" 

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

			      (r * s) ^^^ n = r ^^^ n * s ^^^ n" 

  realpow_minus_oneI:      "-1 ^^^ (2 * n) = 1"  

  realpow_twoI:            "r ^^^ 2 = r * r"

  realpow_twoI_assoc_l:	  "r * (r * s) = r ^^^ 2 * s"

  realpow_twoI_assoc_r:	  "s * r * r = s * r ^^^ 2"

  realpow_two_atom:        "r is_atom ==> r * r = r ^^^ 2"

  realpow_plus_1:          "r * r ^^^ n = r ^^^ (n + 1)"         

  realpow_plus_1_assoc_l:  "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" 

  realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" 

  realpow_plus_1_assoc_r:  "s * r * r ^^^ m = s * r ^^^ (1 + m)"

  realpow_plus_1_atom:     "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"

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

			   ==> r ^^^ n = r * r ^^^ (n + -1)"

  realpow_addI_atom:       "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"

  realpow_minus_even:	  "n is_even ==> (- r) ^^^ n = r ^^^ n"

  realpow_minus_odd:       "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"

(* RL 020914 *)

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

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

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

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

  real_plus_binom_pow3:    "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"

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

			    (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"

  real_minus_binom_pow3:   "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"

  real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +

                           -1*b^^^3"

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

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

  real_plus_binom_pow4:   "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)

                           *(a + b)"

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

			   (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)

                           *(a + b)"

  real_plus_binom_pow5:    "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)

                           *(a^^^2 + 2*a*b + b^^^2)"

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

			        (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 

                                + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"

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

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

  real_plus_binom_times:   "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"

  real_minus_binom_times:  "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"

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

  (*real_plus_binom_pow2:  "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)

  real_plus_binom_pow2:    "(a + b)^^^2 = (a + b) * (a + b)"

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

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

			       (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"

  real_minus_binom_pow2:      "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"

  real_minus_binom_pow2_p:    "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"

  real_plus_minus_binom1:     "(a + b)*(a - b) = a^^^2 - b^^^2"

  real_plus_minus_binom1_p:   "(a + b)*(a - b) = a^^^2 + -1*b^^^2"

  real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"

  real_plus_minus_binom2:     "(a - b)*(a + b) = a^^^2 - b^^^2"

  real_plus_minus_binom2_p:   "(a - b)*(a + b) = a^^^2 + -1*b^^^2"

  real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"

  real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"

  real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a^^^2 + -1*b^^^2"

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

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

(* 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"

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

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

				* n + k"

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

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

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

(* 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"

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

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

(* 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"

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

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

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

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

text {* remark on 'polynomials'

        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 ^^^ 1 + 25 * x ^^^ 2"

	     [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"

	     [2]: "x + (-50) * x ^^^ 3"

	     [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 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 ^^^ 2 - 2 * a * b + b ^^^ 2"

	     "4 * x ^^^ 2 - 9 * y ^^^ 2"

[4] 'polynomial_in' (Polynom in): 

   polynomial in 1 variable with arbitrary coefficients

   examples: "2 * x + (-50) * x ^^^ 3"                     (poly in x)

	     "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)

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

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

   examples: "2 * x - 50 * x ^^^ 3"                     (expanded in x)

	     "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)

*}

ML {*

val thy = @{theory};

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

fun is_polyrat_in t v = 

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

   	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")

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

	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = 

            not(coeff_in b v)

	  | 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 eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _  =

    if is_polyrat_in t v 

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

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

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

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

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

local

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

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

    (* FIXME.WN100826 shift this into test--------------

     val v = (term_of o the o (parse thy)) "x";

     val t = (term_of o the o (parse thy)) "1";

     coeff_in t v;

     (*val it = true : bool*)

     val t = (term_of o the o (parse thy)) "a*b+c";

     coeff_in t v;

     (*val it = true : bool*)

     val t = (term_of o the o (parse thy)) "a*x+c";

     coeff_in t v;

     (*val it = false : bool*)

    ----------------------------------------------------*)

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

    	    (t as Const ("op *",_) $ t1 $ 

    	       (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =

    	if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE

      | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =

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

      | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v = 

    	if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE

      | factor_right_deg vv v =

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

    fun mono_deg_in m v =

    	if coeff_in m v then (*case 1*) SOME 0

    	else factor_right_deg m v;

    (* FIXME.WN100826 shift this into test-----------------------------

     val v = (term_of o the o (parse thy)) "x";

     val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";

     mono_deg_in t v;

     (*val it = SOME 7*)

     val t = (term_of o the o (parse thy)) "x^^^7";

     mono_deg_in t v;

     (*val it = SOME 7*)

     val t = (term_of o the o (parse thy)) "(a*b+c)*x";

     mono_deg_in t v;

     (*val it = SOME 1*)

     val t = (term_of o the o (parse thy)) "(a*b+x)*x";

     mono_deg_in t v;

     (*val it = NONE*)

     val t = (term_of o the o (parse thy)) "x";

     mono_deg_in t v;

     (*val it = SOME 1*)

     val t = (term_of o the o (parse thy)) "(a*b+c)";

     mono_deg_in t v;

     (*val it = SOME 0*)

     val t = (term_of o the o (parse thy)) "ab - (a*b)*x";

     mono_deg_in t v;

     (*val it = NONE*)

    ------------------------------------------------------------------*)

    fun expand_deg_in t v =

    	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =

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

    		     SOME d' => edi d' d' t1

		   | NONE => NONE)

    	      | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =

    		(case mono_deg_in t2 v of

    		     SOME d' => edi d' d' t1

		   | NONE => NONE)

    	      | edi d dmax (Const ("op -",_) $ t1 $ t2) =

    		(case mono_deg_in t2 v of

		(*RL  orelse ((d=0) andalso (d'=0)) need to 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 ("op +",_) $ t1 $ t2) =

    		(case mono_deg_in t2 v of

		(*RL  orelse ((d=0) andalso (d'=0)) need to 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 ~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;

    (* FIXME.WN100826 shift this into test-----------------------------

     val v = (term_of o the o (parse thy)) "x";

     val t = (term_of o the o (parse thy)) "a+b";

     expand_deg_in t v;

     (*val it = SOME 0*)   

     val t = (term_of o the o (parse thy)) "(a+b)*x";

     expand_deg_in t v;

     (*SOME 1*)   

     val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";

     expand_deg_in t v;

     (*SOME 1*)   

     val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";

     expand_deg_in t v;

     (*SOME 1*)   

     val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";

     expand_deg_in t v;

    -------------------------------------------------------------------*)   

    fun poly_deg_in t v =

    	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =

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

    		     SOME d' => edi d' d' t1

		   | NONE => NONE)

    	      | edi d dmax (Const ("op +",_) $ t1 $ t2) =

    		(case mono_deg_in t2 v of

 		(*RL  orelse ((d=0) andalso (d'=0)) need to 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 ~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;

in

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;

end;

(* FIXME.WN100826 shift this into test-----------------------------

 val v = (term_of o the o (parse thy)) "x";

 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";

 has_degree_in t v;

 (*val it = 2*)

 val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";

 has_degree_in t v;

 (*val it = 2*)

 val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";

 has_degree_in t v;

 (*val it = 2*)

-------------------------------------------------------------------*)

(*("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 ((term2str p) ^ " = True",

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

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

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

  | eval_is_expanded_in _ _ _ _ = NONE;

(*

 val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";

 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;

 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)

 term2str t';

 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)

*)

(*("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 ((term2str p) ^ " = True",

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

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

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

  | eval_is_poly_in _ _ _ _ = NONE;

(*

 val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";

 val SOME (id, t') = eval_is_poly_in 0 0 t 0;

 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)

 term2str t';

 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)

*)

(*("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' = term_of_num HOLogic.realT d

    in SOME ((term2str p) ^ " = " ^ (string_of_int d),

	      Trueprop $ (mk_equality (p, d')))

    end

  | eval_has_degree_in _ _ _ _ = NONE;

(*

> val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";

> val SOME (id, t') = eval_has_degree_in 0 0 t 0;

val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string

> term2str t';

val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string

*)

(*..*)

val calculate_Poly =

    append_rls "calculate_PolyFIXXXME.not.impl." e_rls

	       [];

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

val Poly_erls = 

    append_rls "Poly_erls" Atools_erls

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

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

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

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

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

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

		 ];

val poly_crls = 

    append_rls "poly_crls" Atools_crls

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

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

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

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

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

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

		 ];

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

     "Atools.pow" => ((("|||||||||||||", 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);

fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)

    	(case int_of_str (order) of

	             SOME d => d

		   | NONE   => 0)

  | get_order_pow _ = 0;

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

  if "Atools.pow"= 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 _=writeln("t= f@ts= \""^

	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^

	      (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\"");

	   val _=writeln("u= g@us= \""^

	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^

	      (commas(map(Syntax.string_of_term (thy2ctxt thy))us))^"]\"");

	   val _=writeln("size_of_term(t,u)= ("^

	      (string_of_int(size_of_term' t))^", "^

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

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

	   val _=writeln("terms_ord(ts,us) = "^

			   ((pr_ord o terms_ord str false)(ts,us)));

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

	 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 str pr (ts, us) = 

    list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);

in

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

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

end;(*local*)

rew_ord' := overwritel (!rew_ord',

[("termlessI", termlessI),

 ("ord_make_polynomial", ord_make_polynomial false thy)

 ]);

val expand =

  Rls{id = "expand", preconds = [], rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls, calc = [],

      rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),

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

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

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

	       ], scr = EmptyScr}:rls;

(*----------------- Begin: rulesets for make_polynomial_ -----------------

  'rlsIDs' redefined by MG as 'rlsIDs_' 

                                    ^^^*)

val discard_minus1 = 

  Rls{id = "discard_minus1", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),

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

	       Thm ("sym_real_mult_minus1",

                     num_str (@{thm real_mult_minus1} RS @{thm sym}))

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

	       ], scr = EmptyScr}:rls;

val expand_poly_ = 

  Rls{id = "expand_poly_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),

	       (*"(a + b)^^^4 = ... "*)

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

	       (*"(a + b)^^^5 = ... "*)

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

	       (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)

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

	       (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)

	       (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)

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

	       (*"(a + b)^^^2 = (a + b) * (a + b)"*)

	       (*Thm ("real_plus_minus_binom1_p_p",

		    num_str @{thm real_plus_minus_binom1_p_p}),*)

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

	       (*Thm ("real_plus_minus_binom2_p_p",

		    num_str @{thm real_plus_minus_binom2_p_p}),*)

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

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

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

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

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

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

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

	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)

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

	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

	       ], scr = EmptyScr}:rls;

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

   this is weaker than 'is_polynomial' !.*)

fun is_polyexp (Free _) = true

  | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true

  | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true

  | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true

  | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true

  | is_polyexp (Const ("op +",_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const ("op -",_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const ("op *",_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = 

               ((is_polyexp t1) andalso (is_polyexp t2))

  | is_polyexp _ = false;

(*("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 (mk_thmid thmid "" 

			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

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

    else SOME (mk_thmid thmid "" 

			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

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

  | eval_is_polyexp _ _ _ _ = NONE; 

val expand_poly_rat_ = 

  Rls{id = "expand_poly_rat_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls =  append_rls "e_rls-is_polyexp" e_rls

	        [Calc ("Poly.is'_polyexp", eval_is_polyexp "")

		 ],

      srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = 

        [Thm ("real_plus_binom_pow4_poly", num_str @{thm real_plus_binom_pow4_poly}),

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

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

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

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

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

		            (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)

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

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

			(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)

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

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

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

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

	 Thm ("real_add_mult_distrib_poly",

               num_str @{thm real_add_mult_distrib_poly}),

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

	 Thm("real_add_mult_distrib2_poly",

              num_str @{thm real_add_mult_distrib2_poly}),

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

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

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

		            (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)

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

	      (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

	 ], scr = EmptyScr}:rls;

val simplify_power_ = 

  Rls{id = "simplify_power_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls, srls = Erls,

      calc = [],

      (*asm_thm = [],*)

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

		a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)

	       Thm ("sym_realpow_twoI",

                     num_str (@{thm realpow_twoI} RS @{thm sym})),	

	       (*"r * r = r ^^^ 2"*)

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

	       (*"r * (r * s) = r ^^^ 2 * s"*)

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

	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

	       Thm ("realpow_plus_1_assoc_l",

                     num_str @{thm realpow_plus_1_assoc_l}),

	       (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)

	       (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)

	       Thm ("realpow_plus_1_assoc_l2",

                     num_str @{thm realpow_plus_1_assoc_l2}),

	       (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)

	       Thm ("sym_realpow_addI",

               num_str (@{thm realpow_addI} RS @{thm sym})),

	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)

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

	       (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)

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

		  "r * r = r ^^^ 2" wenn r=a^^^b*)

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

	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

	       ], scr = EmptyScr}:rls;

val calc_add_mult_pow_ = 

  Rls{id = "calc_add_mult_pow_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls(*erls3.4.03*),srls = Erls,

      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 

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

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

	      ],

      (*asm_thm = [],*)

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

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

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

	       ], scr = EmptyScr}:rls;

val reduce_012_mult_ = 

  Rls{id = "reduce_012_mult_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

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

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

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

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

	       (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)

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

	       (*"r ^^^ 1 = r"*)

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

	       (*"1 ^^^ n = 1"*)

	       ], scr = EmptyScr}:rls;

val collect_numerals_ = 

  Rls{id = "collect_numerals_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls, srls = Erls,

      calc = [("PLUS"  , ("op +", eval_binop "#add_"))

	      ],

      rules = 

        [Thm ("real_num_collect",num_str @{thm real_num_collect}), 

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

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

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

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

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

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

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

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

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

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

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

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

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

	 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym}))

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

	], scr = EmptyScr}:rls;

val reduce_012_ = 

  Rls{id = "reduce_012_", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls, calc = [],

      rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),                 

	       (*"1 * z = z"*)

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

	       (*"0 * z = 0"*)

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

	       (*"z * 0 = 0"*)

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

	       (*"0 + z = z"*)

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

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

	       (*Thm ("realpow_oneI",num_str @{thm realpow_oneI})*)

	       (*"?r ^^^ 1 = ?r"*)

	       Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)

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

	       ], scr = EmptyScr}:rls;

(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)

val discard_parentheses1 = 

    append_rls "discard_parentheses1" e_rls 

	       [Thm ("sym_real_mult_assoc",

                      num_str (@{thm real_mult_assoc} RS @{thm sym}))

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

		(*Thm ("sym_add_assoc",

                        num_str (@{thm add_assoc} RS @{thm sym}))*)

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

		 ];

(*----------------- End: rulesets for make_polynomial_ -----------------*)

(*MG.0401 ev. for use in rls with ordered rewriting ?

val collect_numerals_left = 

  Rls{id = "collect_numerals", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls(*erls3.4.03*),srls = Erls,

      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 

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

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

	      ],

      (*asm_thm = [],*)

      rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), 

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

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

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

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

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

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

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

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

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

	       (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)

	       Thm ("sym_real_mult_2",

                     num_str (@{thm real_mult_2} RS @{thm sym})),	

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

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

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

	       ], scr = EmptyScr}:rls;*)

val expand_poly = 

  Rls{id = "expand_poly", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),

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

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

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

	       (*Thm ("left_distrib1",num_str @{thm left_distrib}1),

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

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

	       (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)

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

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

	       Thm ("real_plus_minus_binom1_p",

		    num_str @{thm real_plus_minus_binom1_p}),

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

	       Thm ("real_plus_minus_binom2_p",

		    num_str @{thm real_plus_minus_binom2_p}),

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

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

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

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

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

	       Thm ("sym_real_mult_minus1",

                     num_str (@{thm real_mult_minus1} RS @{thm sym}))

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

	       (*Thm ("real_minus_add_distrib",

		      num_str @{thm real_minus_add_distrib}),*)

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

	       (*Thm ("real_diff_plus",num_str @{thm real_diff_plus})*)

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

	       ], scr = EmptyScr}:rls;

val simplify_power = 

  Rls{id = "simplify_power", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls, srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),

	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)

	       Thm ("sym_realpow_twoI",

                     num_str( @{thm realpow_twoI} RS @{thm sym})),	

	       (*"r1 * r1 = r1 ^^^ 2"*)

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

	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

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

	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

	       Thm ("sym_realpow_addI",

                     num_str (@{thm realpow_addI} RS @{thm sym})),

	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)

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

	       (*"r ^^^ 1 = r"*)

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

	       (*"1 ^^^ n = 1"*)

	       ], scr = EmptyScr}:rls;

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

  Rls{id = "order_add_mult", preconds = [], 

      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),

	       (* z * w = w * z *)

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

	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

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

	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

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

	       (*z + w = w + z*)

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

	       (*x + (y + z) = y + (x + z)*)

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

	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

	       ], scr = EmptyScr}:rls;

(*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_mult = 

  Rls{id = "order_mult", preconds = [], 

      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),

	       (* z * w = w * z *)

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

	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

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

	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

	       ], scr = EmptyScr}:rls;

val collect_numerals = 

  Rls{id = "collect_numerals", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls(*erls3.4.03*),srls = Erls,

      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 

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

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

	      ],

      (*asm_thm = [],*)

      rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), 

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

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

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

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

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

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

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

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

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

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

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

	       ], scr = EmptyScr}:rls;

val reduce_012 = 

  Rls{id = "reduce_012", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = e_rls,srls = Erls,

      calc = [],

      (*asm_thm = [],*)

      rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),                 

	       (*"1 * z = z"*)

	       (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03*)

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

	       Thm ("minus_mult_left", 

		    num_str (@{thm minus_mult_left} RS @{thm sym})),

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

	       (*Thm ("real_minus_mult_cancel",

                       num_str @{thm real_minus_mult_cancel}),

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

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

	       (*"0 * z = 0"*)

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

	       (*"0 + z = z"*)

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

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

	       Thm ("sym_real_mult_2",

                     num_str (@{thm real_mult_2} RS @{thm sym})),	

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

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

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

	       ], scr = EmptyScr}:rls;

(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)

val discard_parentheses = 

    append_rls "discard_parentheses" e_rls 

	       [Thm ("sym_real_mult_assoc",

                      num_str (@{thm real_mult_assoc} RS @{thm sym})),

		Thm ("sym_add_assoc",

                      num_str (@{thm add_assoc} RS @{thm sym}))];

val scr_make_polynomial = 

"Script Expand_binoms t_t =                                  " ^

"(Repeat                                                    " ^

"((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 

" (Try (Repeat (Rewrite left_distrib   False))) @@ " ^	 

" (Try (Repeat (Rewrite right_distrib  False))) @@ " ^	

" (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	

" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	

" (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   

" (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   

" (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 

" (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		

" (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	

" (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		

" (Try (Repeat (Rewrite add_commute        False))) @@ " ^		

" (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 

" (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 

" (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 

" (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 

" (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		

" (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		

" (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^		

" (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^	

" (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^		

" (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^   

" (Try (Repeat (Calculate PLUS  ))) @@                      " ^

" (Try (Repeat (Calculate TIMES ))) @@                      " ^

" (Try (Repeat (Calculate POWER))))                        " ^  

" t_t)";

(*version used by MG.02/03, overwritten by version AG in 04 below

val make_polynomial = prep_rls(

  Seq{id = "make_polynomial", preconds = []:term list, 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls, srls = Erls,

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

      rules = [Rls_ expand_poly,

	       Rls_ order_add_mult,

	       Rls_ simplify_power,   (*realpow_eq_oneI, eg. x^1 --> x *)

	       Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1          *)

	       Rls_ reduce_012,

	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),(*in --^*) 

	       Rls_ discard_parentheses

	       ],

      scr = EmptyScr

      }:rls);   *)

val scr_expand_binoms =

"Script Expand_binoms t_t =" ^