
neuper@37906: (* WN.020812: theorems in the Reals,
neuper@37906:    necessary for special rule sets, in addition to Isabelle2002.
neuper@37906:    !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@37906:    !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
neuper@37906:    !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@37906:    xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
neuper@37906:    changed by: Richard Lang 020912
neuper@37906: *)
neuper@37906: 
neuper@37950: theory Poly imports Simplify begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _") 
neuper@37950:   is'_poly'_in     :: "[real, real] => bool" ("_ is'_poly'_in _")   (*RL DA *)
neuper@37950:   has'_degree'_in  :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
neuper@37950:   is'_polyrat'_in  :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
neuper@37906: 
neuper@37950:   is'_multUnordered:: "real => bool" ("_ is'_multUnordered") 
neuper@37950:   is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
neuper@37950:   is'_polyexp      :: "real => bool" ("_ is'_polyexp") 
neuper@37906: 
neuper@37906:   Expand'_binoms
neuper@37950:              :: "['y, 
neuper@37950: 		    'y] => 'y"
neuper@37950:                ("((Script Expand'_binoms (_ =))// 
neuper@37950:                     (_))" 9)
neuper@37906: 
neuper@37906: (*-------------------- rules------------------------------------------------*)
neuper@37950: axioms (*.not contained in Isabelle2002,
neuper@37906:          stated as axioms, TODO: prove as theorems;
neuper@37906:          theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
neuper@37906: 
neuper@37974:   realpow_pow:             "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
neuper@37974:   realpow_addI:            "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
neuper@37974:   realpow_addI_assoc_l:    "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
neuper@37974:   realpow_addI_assoc_r:    "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
neuper@37906: 		  
neuper@37974:   realpow_oneI:            "r ^^^ 1 = r"
neuper@37974:   realpow_zeroI:            "r ^^^ 0 = 1"
neuper@37974:   realpow_eq_oneI:         "1 ^^^ n = 1"
neuper@37974:   realpow_multI:           "(r * s) ^^^ n = r ^^^ n * s ^^^ n" 
neuper@37974:   realpow_multI_poly:      "[| r is_polyexp; s is_polyexp |] ==>
neuper@37950: 			      (r * s) ^^^ n = r ^^^ n * s ^^^ n" 
neuper@37974:   realpow_minus_oneI:      "-1 ^^^ (2 * n) = 1"  
neuper@37906: 
neuper@37974:   realpow_twoI:            "r ^^^ 2 = r * r"
neuper@37974:   realpow_twoI_assoc_l:	  "r * (r * s) = r ^^^ 2 * s"
neuper@37974:   realpow_twoI_assoc_r:	  "s * r * r = s * r ^^^ 2"
neuper@37974:   realpow_two_atom:        "r is_atom ==> r * r = r ^^^ 2"
neuper@37974:   realpow_plus_1:          "r * r ^^^ n = r ^^^ (n + 1)"         
neuper@37974:   realpow_plus_1_assoc_l:  "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" 
neuper@37974:   realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" 
neuper@37974:   realpow_plus_1_assoc_r:  "s * r * r ^^^ m = s * r ^^^ (1 + m)"
neuper@37974:   realpow_plus_1_atom:     "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
neuper@37974:   realpow_def_atom:        "[| Not (r is_atom); 1 < n |]
neuper@37950: 			   ==> r ^^^ n = r * r ^^^ (n + -1)"
neuper@37974:   realpow_addI_atom:       "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
neuper@37906: 
neuper@37906: 
neuper@37974:   realpow_minus_even:	  "n is_even ==> (- r) ^^^ n = r ^^^ n"
neuper@37974:   realpow_minus_odd:       "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
neuper@37906: 
neuper@37906: 
neuper@37906: (* RL 020914 *)
neuper@37974:   real_pp_binom_times:     "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
neuper@37974:   real_pm_binom_times:     "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
neuper@37974:   real_mp_binom_times:     "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
neuper@37974:   real_mm_binom_times:     "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
neuper@37974:   real_plus_binom_pow3:    "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
neuper@37974:   real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==> 
neuper@37950: 			    (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
neuper@37974:   real_minus_binom_pow3:   "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
neuper@37974:   real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
neuper@37950:                            -1*b^^^3"
neuper@37974: (* real_plus_binom_pow:        "[| n is_const;  3 < n |] ==>
neuper@37950: 			       (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
neuper@37974:   real_plus_binom_pow4:   "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
neuper@37950:                            *(a + b)"
neuper@37974:   real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==> 
neuper@37950: 			   (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
neuper@37950:                            *(a + b)"
neuper@37974:   real_plus_binom_pow5:    "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
neuper@37950:                            *(a^^^2 + 2*a*b + b^^^2)"
neuper@37974:   real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==> 
neuper@37950: 			        (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 
neuper@37950:                                 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
neuper@37974:   real_diff_plus:          "a - b = a + -b" (*17.3.03: do_NOT_use*)
neuper@37974:   real_diff_minus:         "a - b = a + -1 * b"
neuper@37974:   real_plus_binom_times:   "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
neuper@37974:   real_minus_binom_times:  "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
neuper@37906:   (*WN071229 changed for Schaerding -----vvv*)
neuper@37974:   (*real_plus_binom_pow2:  "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
neuper@37974:   real_plus_binom_pow2:    "(a + b)^^^2 = (a + b) * (a + b)"
neuper@37906:   (*WN071229 changed for Schaerding -----^^^*)
neuper@37974:   real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
neuper@37950: 			       (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
neuper@37974:   real_minus_binom_pow2:      "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
neuper@37974:   real_minus_binom_pow2_p:    "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
neuper@37974:   real_plus_minus_binom1:     "(a + b)*(a - b) = a^^^2 - b^^^2"
neuper@37974:   real_plus_minus_binom1_p:   "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
neuper@37974:   real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
neuper@37974:   real_plus_minus_binom2:     "(a - b)*(a + b) = a^^^2 - b^^^2"
neuper@37974:   real_plus_minus_binom2_p:   "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
neuper@37974:   real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
neuper@37974:   real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
neuper@37974:   real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a^^^2 + -1*b^^^2"
neuper@37906: 
neuper@37974:   real_num_collect:           "[| l is_const; m is_const |] ==>
neuper@37950: 			      l * n + m * n = (l + m) * n"
neuper@37906: (* FIXME.MG.0401: replace 'real_num_collect_assoc' 
neuper@37906: 	by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
neuper@37974:   real_num_collect_assoc:     "[| l is_const; m is_const |] ==> 
neuper@37950: 			      l * n + (m * n + k) = (l + m) * n + k"
neuper@37974:   real_num_collect_assoc_l:   "[| l is_const; m is_const |] ==>
neuper@37950: 			      l * n + (m * n + k) = (l + m)
neuper@37950: 				* n + k"
neuper@37974:   real_num_collect_assoc_r:   "[| l is_const; m is_const |] ==>
neuper@37950: 			      (k + m * n) + l * n = k + (l + m) * n"
neuper@37974:   real_one_collect:           "m is_const ==> n + m * n = (1 + m) * n"
neuper@37906: (* FIXME.MG.0401: replace 'real_one_collect_assoc' 
neuper@37906: 	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
neuper@37974:   real_one_collect_assoc:     "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
neuper@37906: 
neuper@37974:   real_one_collect_assoc_l:   "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
neuper@37974:   real_one_collect_assoc_r:  "m is_const ==> (k + n) +  m * n = k + (1 + m) * n"
neuper@37906: 
neuper@37906: (* FIXME.MG.0401: replace 'real_mult_2_assoc' 
neuper@37906: 	by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
neuper@37974:   real_mult_2_assoc:          "z1 + (z1 + k) = 2 * z1 + k"
neuper@37974:   real_mult_2_assoc_l:        "z1 + (z1 + k) = 2 * z1 + k"
neuper@37974:   real_mult_2_assoc_r:        "(k + z1) + z1 = k + 2 * z1"
neuper@37906: 
neuper@37974:   real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
neuper@37974:   real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
neuper@37950: 
neuper@37950: text {* remark on 'polynomials'
neuper@37950:         WN020919
neuper@37950: *** there are 5 kinds of expanded normalforms ***
neuper@37950: 
neuper@37950: [1] 'complete polynomial' (Komplettes Polynom), univariate
neuper@37950:    a_0 + a_1.x^1 +...+ a_n.x^n   not (a_n = 0)
neuper@37950: 	        not (a_n = 0), some a_i may be zero (DON'T disappear),
neuper@37950:                 variables in monomials lexicographically ordered and complete,
neuper@37950:                 x written as 1*x^1, ...
neuper@37950: [2] 'polynomial' (Polynom), univariate and multivariate
neuper@37950:    a_0 + a_1.x +...+ a_n.x^n   not (a_n = 0)
neuper@37950:    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
neuper@37950: 	        not (a_n = 0), some a_i may be zero (ie. monomials disappear),
neuper@37950:                 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
neuper@37950:                 and variables in monomials are lexicographically ordered  
neuper@37950:    examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
neuper@37950: 	     [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
neuper@37950: 	     [2]: "x + (-50) * x ^^^ 3"
neuper@37950: 	     [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
neuper@37950: 
neuper@37950: [3] 'expanded_term' (Ausmultiplizierter Term):
neuper@37950:    pull out unary minus to binary minus, 
neuper@37950:    as frequently exercised in schools; other conditions for [2] hold however
neuper@37950:    examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
neuper@37950: 	     "4 * x ^^^ 2 - 9 * y ^^^ 2"
neuper@37950: [4] 'polynomial_in' (Polynom in): 
neuper@37950:    polynomial in 1 variable with arbitrary coefficients
neuper@37950:    examples: "2 * x + (-50) * x ^^^ 3"                     (poly in x)
neuper@37950: 	     "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
neuper@37950: [5] 'expanded_in' (Ausmultiplizierter Termin in): 
neuper@37950:    analoguous to [3] with binary minus like [3]
neuper@37950:    examples: "2 * x - 50 * x ^^^ 3"                     (expanded in x)
neuper@37950: 	     "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
neuper@37950: *}
neuper@37950: 
neuper@37950: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37950: (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
neuper@37950: fun is_polyrat_in t v = 
neuper@37950:     let fun coeff_in c v = member op = (vars c) v;
neuper@38031:    	fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
neuper@37950: 	    (* at the moment there is no term like this, but ....*)
neuper@38014: 	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = 
neuper@37950:             not(coeff_in b v)
neuper@37950: 	  | finddivide (_ $ t1 $ t2) v = 
neuper@37950:             (finddivide t1 v) orelse (finddivide t2 v)
neuper@37950: 	  | finddivide (_ $ t1) v = (finddivide t1 v)
neuper@37950: 	  | finddivide _ _ = false;
neuper@37950:      in finddivide t v end;
neuper@37950:     
neuper@37950: fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _  =
neuper@37950:     if is_polyrat_in t v 
neuper@37950:     then SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@38015:   | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
neuper@37950: 
neuper@37950: local
neuper@37950:     (*.a 'c is coefficient of v' if v does NOT occur in c.*)
neuper@37950:     fun coeff_in c v = not (member op = (vars c) v);
neuper@37950:     (* FIXME.WN100826 shift this into test--------------
neuper@37950:      val v = (term_of o the o (parse thy)) "x";
neuper@37950:      val t = (term_of o the o (parse thy)) "1";
neuper@37950:      coeff_in t v;
neuper@37950:      (*val it = true : bool*)
neuper@37950:      val t = (term_of o the o (parse thy)) "a*b+c";
neuper@37950:      coeff_in t v;
neuper@37950:      (*val it = true : bool*)
neuper@37950:      val t = (term_of o the o (parse thy)) "a*x+c";
neuper@37950:      coeff_in t v;
neuper@37950:      (*val it = false : bool*)
neuper@37950:     ----------------------------------------------------*)
neuper@37950:     (*. a 'monomial t in variable v' is a term t with
neuper@37950:       either (1) v NOT existent in t, or (2) v contained in t,
neuper@37950:       if (1) then degree 0
neuper@37950:       if (2) then v is a factor on the very right, ev. with exponent.*)
neuper@37950:     fun factor_right_deg (*case 2*)
neuper@37950:     	    (t as Const ("op *",_) $ t1 $ 
neuper@37950:     	       (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
neuper@37950:     	if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
neuper@37950:       | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
neuper@37950:     	if (vv = v) then SOME (int_of_str' d) else NONE
neuper@37950:       | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v = 
neuper@37950:     	if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
neuper@37950:       | factor_right_deg vv v =
neuper@37950:     	if (vv = v) then SOME 1 else NONE;    
neuper@37950:     fun mono_deg_in m v =
neuper@37950:     	if coeff_in m v then (*case 1*) SOME 0
neuper@37950:     	else factor_right_deg m v;
neuper@37950:     (* FIXME.WN100826 shift this into test-----------------------------
neuper@37950:      val v = (term_of o the o (parse thy)) "x";
neuper@37950:      val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = SOME 7*)
neuper@37950:      val t = (term_of o the o (parse thy)) "x^^^7";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = SOME 7*)
neuper@37950:      val t = (term_of o the o (parse thy)) "(a*b+c)*x";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = SOME 1*)
neuper@37950:      val t = (term_of o the o (parse thy)) "(a*b+x)*x";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = NONE*)
neuper@37950:      val t = (term_of o the o (parse thy)) "x";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = SOME 1*)
neuper@37950:      val t = (term_of o the o (parse thy)) "(a*b+c)";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = SOME 0*)
neuper@37950:      val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
neuper@37950:      mono_deg_in t v;
neuper@37950:      (*val it = NONE*)
neuper@37950:     ------------------------------------------------------------------*)
neuper@37950:     fun expand_deg_in t v =
neuper@38014:     	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of (* $ is left associative*)
neuper@37950:     		     SOME d' => edi d' d' t1
neuper@37950: 		   | NONE => NONE)
neuper@38014:     	      | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of
neuper@37950:     		     SOME d' => edi d' d' t1
neuper@37950: 		   | NONE => NONE)
neuper@38014:     	      | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of
neuper@37950: 		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
neuper@37950:     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
neuper@37950:                      then edi d' dmax t1 else NONE
neuper@37950: 		   | NONE => NONE)
neuper@38014:     	      | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of
neuper@37950: 		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
neuper@37950:     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
neuper@37950:                      then edi d' dmax t1 else NONE
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	      | edi ~1 ~1 t = (case mono_deg_in t v of
neuper@37950:     		     d as SOME _ => d
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	      | edi d dmax t = (*basecase last*)
neuper@37950:     		(case mono_deg_in t v of
neuper@37950:     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))  
neuper@37950:                      then SOME dmax else NONE
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	in edi ~1 ~1 t end;
neuper@37950:     (* FIXME.WN100826 shift this into test-----------------------------
neuper@37950:      val v = (term_of o the o (parse thy)) "x";
neuper@37950:      val t = (term_of o the o (parse thy)) "a+b";
neuper@37950:      expand_deg_in t v;
neuper@37950:      (*val it = SOME 0*)   
neuper@37950:      val t = (term_of o the o (parse thy)) "(a+b)*x";
neuper@37950:      expand_deg_in t v;
neuper@37950:      (*SOME 1*)   
neuper@37950:      val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
neuper@37950:      expand_deg_in t v;
neuper@37950:      (*SOME 1*)   
neuper@37950:      val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
neuper@37950:      expand_deg_in t v;
neuper@37950:      (*SOME 1*)   
neuper@37950:      val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
neuper@37950:      expand_deg_in t v;
neuper@37950:     -------------------------------------------------------------------*)   
neuper@37950:     fun poly_deg_in t v =
neuper@38014:     	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of (* $ is left associative*)
neuper@37950:     		     SOME d' => edi d' d' t1
neuper@37950: 		   | NONE => NONE)
neuper@38014:     	      | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950:     		(case mono_deg_in t2 v of
neuper@37950:  		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
neuper@37950:    		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
neuper@37950:                                 then edi d' dmax t1 else NONE
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	      | edi ~1 ~1 t = (case mono_deg_in t v of
neuper@37950:     		     d as SOME _ => d
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	      | edi d dmax t = (*basecase last*)
neuper@37950:     		(case mono_deg_in t v of
neuper@37950:     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
neuper@37950:                      then SOME dmax else NONE
neuper@37950: 		   | NONE => NONE)
neuper@37950:     	in edi ~1 ~1 t end;
neuper@37950: in
neuper@37950: 
neuper@37950: fun is_expanded_in t v =
neuper@37950:     case expand_deg_in t v of SOME _ => true | NONE => false;
neuper@37950: fun is_poly_in t v =
neuper@37950:     case poly_deg_in t v of SOME _ => true | NONE => false;
neuper@37950: fun has_degree_in t v =
neuper@37950:     case expand_deg_in t v of SOME d => d | NONE => ~1;
neuper@37980: end;(*local*)
neuper@37950: (* FIXME.WN100826 shift this into test-----------------------------
neuper@37950:  val v = (term_of o the o (parse thy)) "x";
neuper@37950:  val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
neuper@37950:  has_degree_in t v;
neuper@37950:  (*val it = 2*)
neuper@37950:  val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
neuper@37950:  has_degree_in t v;
neuper@37950:  (*val it = 2*)
neuper@37950:  val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
neuper@37950:  has_degree_in t v;
neuper@37950:  (*val it = 2*)
neuper@37950: -------------------------------------------------------------------*)
neuper@37950: 
neuper@37950: (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
neuper@37950: fun eval_is_expanded_in _ _ 
neuper@37950:        (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
neuper@37950:     if is_expanded_in t v
neuper@37950:     then SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_is_expanded_in _ _ _ _ = NONE;
neuper@37950: (*
neuper@37950:  val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
neuper@37950:  val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
neuper@37950:  (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
neuper@37950:  term2str t';
neuper@37950:  (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
neuper@37950: *)
neuper@37950: 
neuper@37950: (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
neuper@37950: fun eval_is_poly_in _ _ 
neuper@37950:        (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
neuper@37950:     if is_poly_in t v
neuper@37950:     then SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	        Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_is_poly_in _ _ _ _ = NONE;
neuper@37950: (*
neuper@37950:  val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
neuper@37950:  val SOME (id, t') = eval_is_poly_in 0 0 t 0;
neuper@37950:  (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
neuper@37950:  term2str t';
neuper@37950:  (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
neuper@37950: *)
neuper@37950: 
neuper@37950: (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
neuper@37950: fun eval_has_degree_in _ _ 
neuper@37950: 	     (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
neuper@37950:     let val d = has_degree_in t v
neuper@37950: 	val d' = term_of_num HOLogic.realT d
neuper@37950:     in SOME ((term2str p) ^ " = " ^ (string_of_int d),
neuper@37950: 	      Trueprop $ (mk_equality (p, d')))
neuper@37950:     end
neuper@37950:   | eval_has_degree_in _ _ _ _ = NONE;
neuper@37950: (*
neuper@37950: > val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
neuper@37950: > val SOME (id, t') = eval_has_degree_in 0 0 t 0;
neuper@37950: val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
neuper@37950: > term2str t';
neuper@37950: val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
neuper@37950: *)
neuper@37950: 
neuper@37978: (*..*)
neuper@37978: val calculate_Poly =
neuper@37978:     append_rls "calculate_PolyFIXXXME.not.impl." e_rls
neuper@37978: 	       [];
neuper@37978: 
neuper@37950: (*.for evaluation of conditions in rewrite rules.*)
neuper@37950: val Poly_erls = 
neuper@37950:     append_rls "Poly_erls" Atools_erls
neuper@37950:                [ Calc ("op =",eval_equal "#equal_"),
neuper@37969: 		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
neuper@38014:                  Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@38014: 		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
neuper@37950: 		 Calc ("op *",eval_binop "#mult_"),
neuper@37950: 		 Calc ("Atools.pow" ,eval_binop "#power_")
neuper@37950: 		 ];
neuper@37950: 
neuper@37950: val poly_crls = 
neuper@37950:     append_rls "poly_crls" Atools_crls
neuper@37950:                [ Calc ("op =",eval_equal "#equal_"),
neuper@37969: 		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
neuper@38014:                  Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@38014: 		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
neuper@37950: 		 Calc ("op *",eval_binop "#mult_"),
neuper@37950: 		 Calc ("Atools.pow" ,eval_binop "#power_")
neuper@37950: 		 ];
neuper@37950: 
neuper@37950: local (*. for make_polynomial .*)
neuper@37950: 
neuper@37950: open Term;  (* for type order = EQUAL | LESS | GREATER *)
neuper@37950: 
neuper@37950: fun pr_ord EQUAL = "EQUAL"
neuper@37950:   | pr_ord LESS  = "LESS"
neuper@37950:   | pr_ord GREATER = "GREATER";
neuper@37950: 
neuper@37950: fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
neuper@37950:   (case a of
neuper@37950:      "Atools.pow" => ((("|||||||||||||", 0), T), 0)    (*WN greatest string*)
neuper@37950:    | _ => (((a, 0), T), 0))
neuper@37950:   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
neuper@37950:   | dest_hd' (Var v) = (v, 2)
neuper@37950:   | dest_hd' (Bound i) = ((("", i), dummyT), 3)
neuper@37950:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37950: 
neuper@37950: fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
neuper@37950:     	(case int_of_str (order) of
neuper@37950: 	             SOME d => d
neuper@37950: 		   | NONE   => 0)
neuper@37950:   | get_order_pow _ = 0;
neuper@37950: 
neuper@37950: fun size_of_term' (Const(str,_) $ t) =
neuper@37950:   if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
neuper@37950:   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
neuper@37950:   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
neuper@37950:   | size_of_term' _ = 1;
neuper@37950: 
neuper@37950: fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
neuper@37974:       (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
neuper@37950:   | term_ord' pr thy (t, u) =
neuper@37950:       (if pr then 
neuper@37950: 	 let
neuper@37950: 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@38015: 	   val _=tracing("t= f@ts= \""^
neuper@37950: 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
neuper@37950: 	      (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\"");
neuper@38015: 	   val _=tracing("u= g@us= \""^
neuper@37950: 	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
neuper@37950: 	      (commas(map(Syntax.string_of_term (thy2ctxt thy))us))^"]\"");
neuper@38015: 	   val _=tracing("size_of_term(t,u)= ("^
neuper@37950: 	      (string_of_int(size_of_term' t))^", "^
neuper@37950: 	      (string_of_int(size_of_term' u))^")");
neuper@38015: 	   val _=tracing("hd_ord(f,g)      = "^((pr_ord o hd_ord)(f,g)));
neuper@38015: 	   val _=tracing("terms_ord(ts,us) = "^
neuper@37950: 			   ((pr_ord o terms_ord str false)(ts,us)));
neuper@38015: 	   val _=tracing("-------");
neuper@37950: 	 in () end
neuper@37950:        else ();
neuper@37950: 	 case int_ord (size_of_term' t, size_of_term' u) of
neuper@37950: 	   EQUAL =>
neuper@37950: 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
neuper@37950: 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 
neuper@37950: 	     | ord => ord)
neuper@37950: 	     end
neuper@37950: 	 | ord => ord)
neuper@37950: and hd_ord (f, g) =                                        (* ~ term.ML *)
neuper@37974:   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
neuper@37950: and terms_ord str pr (ts, us) = 
neuper@37991:     list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
neuper@37950: in
neuper@37950: 
neuper@37950: fun ord_make_polynomial (pr:bool) thy (_:subst) tu = 
neuper@37950:     (term_ord' pr thy(***) tu = LESS );
neuper@37950: 
neuper@37950: end;(*local*)
neuper@37950: 
neuper@37950: 
neuper@37950: rew_ord' := overwritel (!rew_ord',
neuper@37950: [("termlessI", termlessI),
neuper@37950:  ("ord_make_polynomial", ord_make_polynomial false thy)
neuper@37950:  ]);
neuper@37950: 
neuper@37950: 
neuper@37950: val expand =
neuper@37974:   Rls{id = "expand", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
neuper@37974:       erls = e_rls,srls = Erls, calc = [],
neuper@37965:       rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	       Thm ("right_distrib",num_str @{thm right_distrib})
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: (*----------------- Begin: rulesets for make_polynomial_ -----------------
neuper@37950:   'rlsIDs' redefined by MG as 'rlsIDs_' 
neuper@37950:                                     ^^^*)
neuper@37950: 
neuper@37980: val discard_minus =
neuper@37980:   Rls{id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
neuper@37980:       erls = e_rls, srls = Erls, calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37950: 	       (*"a - b = a + -1 * b"*)
neuper@37969: 	       Thm ("sym_real_mult_minus1",
neuper@37974:                      num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@37950: 	       (*- ?z = "-1 * ?z"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37980: 
neuper@37950: val expand_poly_ = 
neuper@37950:   Rls{id = "expand_poly_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
neuper@37950: 	       (*"(a + b)^^^4 = ... "*)
neuper@37969: 	       Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
neuper@37950: 	       (*"(a + b)^^^5 = ... "*)
neuper@37969: 	       Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
neuper@37950: 	       (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
neuper@37950: 	       (*WN071229 changed/removed for Schaerding -----vvv*)
neuper@37969: 	       (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)
neuper@37950: 	       (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
neuper@37969: 	       Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
neuper@37950: 	       (*"(a + b)^^^2 = (a + b) * (a + b)"*)
neuper@37950: 	       (*Thm ("real_plus_minus_binom1_p_p",
neuper@37969: 		    num_str @{thm real_plus_minus_binom1_p_p}),*)
neuper@37950: 	       (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 	       (*Thm ("real_plus_minus_binom2_p_p",
neuper@37969: 		    num_str @{thm real_plus_minus_binom2_p_p}),*)
neuper@37950: 	       (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 	       (*WN071229 changed/removed for Schaerding -----^^^*)
neuper@37950: 	      
neuper@37965: 	       Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	       Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
neuper@37969: 	       Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950: 	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37969: 	       Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950: 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: (*.the expression contains + - * ^ only ?
neuper@37950:    this is weaker than 'is_polynomial' !.*)
neuper@37950: fun is_polyexp (Free _) = true
neuper@38014:   | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
neuper@38014:   | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
neuper@37950:   | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
neuper@37950:   | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
neuper@38014:   | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
neuper@37950:                ((is_polyexp t1) andalso (is_polyexp t2))
neuper@38014:   | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = 
neuper@37950:                ((is_polyexp t1) andalso (is_polyexp t2))
neuper@37950:   | is_polyexp (Const ("op *",_) $ t1 $ t2) = 
neuper@37950:                ((is_polyexp t1) andalso (is_polyexp t2))
neuper@37950:   | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = 
neuper@37950:                ((is_polyexp t1) andalso (is_polyexp t2))
neuper@37950:   | is_polyexp _ = false;
neuper@37950: 
neuper@37950: (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
neuper@37950: fun eval_is_polyexp (thmid:string) _ 
neuper@37950: 		       (t as (Const("Poly.is'_polyexp", _) $ arg)) thy = 
neuper@37950:     if is_polyexp arg
neuper@37950:     then SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950:     else SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950:   | eval_is_polyexp _ _ _ _ = NONE; 
neuper@37950: 
neuper@37950: val expand_poly_rat_ = 
neuper@37950:   Rls{id = "expand_poly_rat_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls =  append_rls "e_rls-is_polyexp" e_rls
neuper@37950: 	        [Calc ("Poly.is'_polyexp", eval_is_polyexp "")
neuper@37950: 		 ],
neuper@37950:       srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37950:       rules = 
neuper@37969:         [Thm ("real_plus_binom_pow4_poly", num_str @{thm real_plus_binom_pow4_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
neuper@37969: 	 Thm ("real_plus_binom_pow5_poly", num_str @{thm real_plus_binom_pow5_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
neuper@37969: 	 Thm ("real_plus_binom_pow2_poly",num_str @{thm real_plus_binom_pow2_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==>
neuper@37950: 		            (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
neuper@37969: 	 Thm ("real_plus_binom_pow3_poly",num_str @{thm real_plus_binom_pow3_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==> 
neuper@37950: 			(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
neuper@37969: 	 Thm ("real_plus_minus_binom1_p_p",num_str @{thm real_plus_minus_binom1_p_p}),
neuper@37950: 	     (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
neuper@37969: 	 Thm ("real_plus_minus_binom2_p_p",num_str @{thm real_plus_minus_binom2_p_p}),
neuper@37950: 	     (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 	      
neuper@37974: 	 Thm ("real_add_mult_distrib_poly",
neuper@37974:                num_str @{thm real_add_mult_distrib_poly}),
neuper@37950: 	       (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	 Thm("real_add_mult_distrib2_poly",
neuper@37974:               num_str @{thm real_add_mult_distrib2_poly}),
neuper@37950: 	     (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
neuper@37969: 	 Thm ("realpow_multI_poly", num_str @{thm realpow_multI_poly}),
neuper@37950: 	     (*"[| r is_polyexp; s is_polyexp |] ==> 
neuper@37950: 		            (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37969: 	  Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950: 	      (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
neuper@37950: 	 ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val simplify_power_ = 
neuper@37950:   Rls{id = "simplify_power_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls, srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37950:       rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
neuper@37950: 		a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
neuper@37969: 	       Thm ("sym_realpow_twoI",
neuper@37969:                      num_str (@{thm realpow_twoI} RS @{thm sym})),	
neuper@37950: 	       (*"r * r = r ^^^ 2"*)
neuper@37969: 	       Thm ("realpow_twoI_assoc_l",num_str @{thm realpow_twoI_assoc_l}),
neuper@37950: 	       (*"r * (r * s) = r ^^^ 2 * s"*)
neuper@37950: 
neuper@37969: 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),		
neuper@37950: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
neuper@37969: 	       Thm ("realpow_plus_1_assoc_l",
neuper@37969:                      num_str @{thm realpow_plus_1_assoc_l}),
neuper@37950: 	       (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
neuper@37950: 	       (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
neuper@37969: 	       Thm ("realpow_plus_1_assoc_l2",
neuper@37969:                      num_str @{thm realpow_plus_1_assoc_l2}),
neuper@37950: 	       (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
neuper@37950: 
neuper@37969: 	       Thm ("sym_realpow_addI",
neuper@37969:                num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950: 	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
neuper@37969: 	       Thm ("realpow_addI_assoc_l",num_str @{thm realpow_addI_assoc_l}),
neuper@37950: 	       (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
neuper@37950: 	       
neuper@37950: 	       (* ist in expand_poly - wird hier aber auch gebraucht, wegen: 
neuper@37950: 		  "r * r = r ^^^ 2" wenn r=a^^^b*)
neuper@37969: 	       Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950: 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val calc_add_mult_pow_ = 
neuper@37950:   Rls{id = "calc_add_mult_pow_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls(*erls3.4.03*),srls = Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@37950: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37950: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950: 	      ],
neuper@37950:       (*asm_thm = [],*)
neuper@38014:       rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val reduce_012_mult_ = 
neuper@37950:   Rls{id = "reduce_012_mult_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37950:       rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
neuper@37965:                Thm ("mult_1_right",num_str @{thm mult_1_right}),
neuper@37950: 	       (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*) 
neuper@37969: 	       Thm ("realpow_zeroI",num_str @{thm realpow_zeroI}),
neuper@37950: 	       (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
neuper@37969: 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
neuper@37950: 	       (*"r ^^^ 1 = r"*)
neuper@37974: 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
neuper@37950: 	       (*"1 ^^^ n = 1"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val collect_numerals_ = 
neuper@37950:   Rls{id = "collect_numerals_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls, srls = Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_"))
neuper@37950: 	      ],
neuper@37950:       rules = 
neuper@37969:         [Thm ("real_num_collect",num_str @{thm real_num_collect}), 
neuper@37950: 	     (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37969: 	 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),
neuper@37950: 	     (*"[| l is_const; m is_const |] ==>  \
neuper@37950: 					\(k + m * n) + l * n = k + (l + m)*n"*)
neuper@37969: 	 Thm ("real_one_collect",num_str @{thm real_one_collect}),	
neuper@37950: 	     (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37969: 	 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}), 
neuper@37950: 	     (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
neuper@37950: 
neuper@38014:          Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@37950: 
neuper@37950: 	 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
neuper@37950: 		     (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
neuper@37969:          Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),
neuper@37950: 	     (*"(k + z1) + z1 = k + 2 * z1"*)
neuper@37969: 	 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym}))
neuper@37950: 	     (*"z1 + z1 = 2 * z1"*)
neuper@37950: 	], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val reduce_012_ = 
neuper@37950:   Rls{id = "reduce_012_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37974:       erls = e_rls,srls = Erls, calc = [],
neuper@37965:       rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),                 
neuper@37950: 	       (*"1 * z = z"*)
neuper@37965: 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),        
neuper@37950: 	       (*"0 * z = 0"*)
neuper@37974: 	       Thm ("mult_zero_right",num_str @{thm mult_zero_right}),
neuper@37950: 	       (*"z * 0 = 0"*)
neuper@37965: 	       Thm ("add_0_left",num_str @{thm add_0_left}),
neuper@37950: 	       (*"0 + z = z"*)
neuper@37965: 	       Thm ("add_0_right",num_str @{thm add_0_right}),
neuper@37950: 	       (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
neuper@37950: 
neuper@37969: 	       (*Thm ("realpow_oneI",num_str @{thm realpow_oneI})*)
neuper@37950: 	       (*"?r ^^^ 1 = ?r"*)
neuper@37965: 	       Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
neuper@37950: 	       (*"0 / ?x = 0"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
neuper@37979: val discard_parentheses1 = 
neuper@37979:     append_rls "discard_parentheses1" e_rls 
neuper@37969: 	       [Thm ("sym_real_mult_assoc",
neuper@37969:                       num_str (@{thm real_mult_assoc} RS @{thm sym}))
neuper@37950: 		(*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
neuper@37974: 		(*Thm ("sym_add_assoc",
neuper@37974:                         num_str (@{thm add_assoc} RS @{thm sym}))*)
neuper@37950: 		(*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
neuper@37950: 		 ];
neuper@37950: 
neuper@37950: (*----------------- End: rulesets for make_polynomial_ -----------------*)
neuper@37950: 
neuper@37950: (*MG.0401 ev. for use in rls with ordered rewriting ?
neuper@37950: val collect_numerals_left = 
neuper@37950:   Rls{id = "collect_numerals", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls(*erls3.4.03*),srls = Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@37950: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37950: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950: 	      ],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), 
neuper@37950: 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37969: 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950: 	       (*"[| l is_const; m is_const |] ==>  
neuper@37950: 				l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37969: 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),	
neuper@37950: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37969: 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	       (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
neuper@37950: 	       
neuper@38014: 	       Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@37950: 
neuper@37950: 	       (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
neuper@37969: 	       Thm ("sym_real_mult_2",
neuper@37969:                      num_str (@{thm real_mult_2} RS @{thm sym})),	
neuper@37950: 	       (*"z1 + z1 = 2 * z1"*)
neuper@37969: 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
neuper@37950: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;*)
neuper@37950: 
neuper@37950: val expand_poly = 
neuper@37950:   Rls{id = "expand_poly", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37965:       rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	       Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37965: 	       (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
neuper@37950: 		....... 18.3.03 undefined???*)
neuper@37950: 
neuper@37969: 	       Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
neuper@37950: 	       (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
neuper@37969: 	       Thm ("real_minus_binom_pow2_p",num_str @{thm real_minus_binom_pow2_p}),
neuper@37950: 	       (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
neuper@37950: 	       Thm ("real_plus_minus_binom1_p",
neuper@37969: 		    num_str @{thm real_plus_minus_binom1_p}),
neuper@37950: 	       (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 	       Thm ("real_plus_minus_binom2_p",
neuper@37969: 		    num_str @{thm real_plus_minus_binom2_p}),
neuper@37950: 	       (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 
neuper@37965: 	       Thm ("minus_minus",num_str @{thm minus_minus}),
neuper@37950: 	       (*"- (- ?z) = ?z"*)
neuper@37969: 	       Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37950: 	       (*"a - b = a + -1 * b"*)
neuper@37969: 	       Thm ("sym_real_mult_minus1",
neuper@37969:                      num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@37950: 	       (*- ?z = "-1 * ?z"*)
neuper@37950: 
neuper@37950: 	       (*Thm ("real_minus_add_distrib",
neuper@37969: 		      num_str @{thm real_minus_add_distrib}),*)
neuper@37950: 	       (*"- (?x + ?y) = - ?x + - ?y"*)
neuper@37969: 	       (*Thm ("real_diff_plus",num_str @{thm real_diff_plus})*)
neuper@37950: 	       (*"a - b = a + -b"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val simplify_power = 
neuper@37950:   Rls{id = "simplify_power", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls, srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950: 	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950: 	       
neuper@37969: 	       Thm ("sym_realpow_twoI",
neuper@37969:                      num_str( @{thm realpow_twoI} RS @{thm sym})),	
neuper@37950: 	       (*"r1 * r1 = r1 ^^^ 2"*)
neuper@37969: 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),		
neuper@37950: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
neuper@37969: 	       Thm ("realpow_pow",num_str @{thm realpow_pow}),
neuper@37950: 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
neuper@37969: 	       Thm ("sym_realpow_addI",
neuper@37969:                      num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950: 	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
neuper@37969: 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
neuper@37950: 	       (*"r ^^^ 1 = r"*)
neuper@37969: 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
neuper@37950: 	       (*"1 ^^^ n = 1"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: (*MG.0401: termorders for multivariate polys dropped due to principal problems:
neuper@37950:   (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
neuper@37950: val order_add_mult = 
neuper@37950:   Rls{id = "order_add_mult", preconds = [], 
neuper@37972:       rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37950: 	       (* z * w = w * z *)
neuper@37969: 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37950: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37969: 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),		
neuper@37950: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37965: 	       Thm ("add_commute",num_str @{thm add_commute}),	
neuper@37950: 	       (*z + w = w + z*)
neuper@37965: 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37950: 	       (*x + (y + z) = y + (x + z)*)
neuper@37965: 	       Thm ("add_assoc",num_str @{thm add_assoc})	               
neuper@37950: 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: (*MG.0401: termorders for multivariate polys dropped due to principal problems:
neuper@37950:   (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
neuper@37950: val order_mult = 
neuper@37950:   Rls{id = "order_mult", preconds = [], 
neuper@37972:       rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37950: 	       (* z * w = w * z *)
neuper@37969: 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37950: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37969: 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc})	
neuper@37950: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: val collect_numerals = 
neuper@37950:   Rls{id = "collect_numerals", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls(*erls3.4.03*),srls = Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@37950: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37950: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950: 	      ],
neuper@37950:       (*asm_thm = [],*)
neuper@37969:       rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), 
neuper@37950: 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37969: 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950: 	       (*"[| l is_const; m is_const |] ==>  
neuper@37950: 				l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37969: 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),	
neuper@37950: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37969: 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@38014: 	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: val reduce_012 = 
neuper@37950:   Rls{id = "reduce_012", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37965:       rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),                 
neuper@37950: 	       (*"1 * z = z"*)
neuper@37969: 	       (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03*)
neuper@37950: 	       (*"-1 * z = - z"*)
neuper@37965: 	       Thm ("minus_mult_left", 
neuper@37974: 		    num_str (@{thm minus_mult_left} RS @{thm sym})),
neuper@37950: 	       (*- (?x * ?y) = "- ?x * ?y"*)
neuper@37969: 	       (*Thm ("real_minus_mult_cancel",
neuper@37969:                        num_str @{thm real_minus_mult_cancel}),
neuper@37950: 	       (*"- ?x * - ?y = ?x * ?y"*)---*)
neuper@37965: 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),        
neuper@37950: 	       (*"0 * z = 0"*)
neuper@37965: 	       Thm ("add_0_left",num_str @{thm add_0_left}),
neuper@37950: 	       (*"0 + z = z"*)
neuper@37965: 	       Thm ("right_minus",num_str @{thm right_minus}),
neuper@37950: 	       (*"?z + - ?z = 0"*)
neuper@37969: 	       Thm ("sym_real_mult_2",
neuper@37969:                      num_str (@{thm real_mult_2} RS @{thm sym})),	
neuper@37950: 	       (*"z1 + z1 = 2 * z1"*)
neuper@37969: 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
neuper@37950: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
neuper@37950: val discard_parentheses = 
neuper@37950:     append_rls "discard_parentheses" e_rls 
neuper@37969: 	       [Thm ("sym_real_mult_assoc",
neuper@37969:                       num_str (@{thm real_mult_assoc} RS @{thm sym})),
neuper@37974: 		Thm ("sym_add_assoc",
neuper@37974:                       num_str (@{thm add_assoc} RS @{thm sym}))];
neuper@37950: 
neuper@37950: val scr_make_polynomial = 
neuper@37976: "Script Expand_binoms t_t =                                  " ^
neuper@37950: "(Repeat                                                    " ^
neuper@37950: "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
neuper@37950: 
neuper@37971: " (Try (Repeat (Rewrite left_distrib   False))) @@ " ^	 
neuper@37971: " (Try (Repeat (Rewrite right_distrib  False))) @@ " ^	
neuper@37971: " (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	
neuper@37971: " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	
neuper@37950: 
neuper@37971: " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   
neuper@37971: " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   
neuper@37971: " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		
neuper@37950: " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	
neuper@37950: " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		
neuper@37971: " (Try (Repeat (Rewrite add_commute        False))) @@ " ^		
neuper@37971: " (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 
neuper@37971: " (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 
neuper@37950: " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 
neuper@37950: " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		
neuper@37950: " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^		
neuper@37950: " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^	
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^		
neuper@37950: " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^   
neuper@37950: 
neuper@37975: " (Try (Repeat (Calculate PLUS  ))) @@                      " ^
neuper@37975: " (Try (Repeat (Calculate TIMES ))) @@                      " ^
neuper@37975: " (Try (Repeat (Calculate POWER))))                        " ^  
neuper@37976: " t_t)";
neuper@37950: 
neuper@37950: (*version used by MG.02/03, overwritten by version AG in 04 below
neuper@37950: val make_polynomial = prep_rls(
neuper@37950:   Seq{id = "make_polynomial", preconds = []:term list, 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls, srls = Erls,
neuper@37950:       calc = [],(*asm_thm = [],*)
neuper@37950:       rules = [Rls_ expand_poly,
neuper@37950: 	       Rls_ order_add_mult,
neuper@37950: 	       Rls_ simplify_power,   (*realpow_eq_oneI, eg. x^1 --> x *)
neuper@37950: 	       Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1          *)
neuper@37950: 	       Rls_ reduce_012,
neuper@37969: 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),(*in --^*) 
neuper@37950: 	       Rls_ discard_parentheses
neuper@37950: 	       ],
neuper@37950:       scr = EmptyScr
neuper@37950:       }:rls);   *)
neuper@37950: 
neuper@37950: val scr_expand_binoms =
neuper@37974: "Script Expand_binoms t_t =" ^
neuper@37950: "(Repeat                       " ^
neuper@37950: "((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^
neuper@37950: 
neuper@37971: " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^
neuper@37971: " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^
neuper@37971: " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^
neuper@37950: 
neuper@37975: " (Try (Repeat (Calculate PLUS  ))) @@ " ^
neuper@37975: " (Try (Repeat (Calculate TIMES ))) @@ " ^
neuper@37975: " (Try (Repeat (Calculate POWER))) @@ " ^
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^
neuper@37950: 
neuper@37950: " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^
neuper@37950: " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^ 
neuper@37950: 
neuper@37975: " (Try (Repeat (Calculate PLUS  ))) @@ " ^
neuper@37975: " (Try (Repeat (Calculate TIMES ))) @@ " ^
neuper@37975: " (Try (Repeat (Calculate POWER)))) " ^  
neuper@37974: " t_t)";
neuper@37974: 
neuper@37950: val expand_binoms = 
neuper@37950:   Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
neuper@37950:       erls = Atools_erls, srls = Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@37950: 	      ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37950: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950: 	      ],
neuper@37974:       rules = [Thm ("real_plus_binom_pow2",
neuper@37974:                      num_str @{thm real_plus_binom_pow2}),     
neuper@37950: 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
neuper@37974: 	       Thm ("real_plus_binom_times",
neuper@37974:                      num_str @{thm real_plus_binom_times}),    
neuper@37950: 	      (*"(a + b)*(a + b) = ...*)
neuper@37974: 	       Thm ("real_minus_binom_pow2",
neuper@37974:                      num_str @{thm real_minus_binom_pow2}),   
neuper@37950: 	       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
neuper@37974: 	       Thm ("real_minus_binom_times",
neuper@37974:                      num_str @{thm real_minus_binom_times}),   
neuper@37950: 	       (*"(a - b)*(a - b) = ...*)
neuper@37974: 	       Thm ("real_plus_minus_binom1",
neuper@37974:                      num_str @{thm real_plus_minus_binom1}),   
neuper@37950: 		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37974: 	       Thm ("real_plus_minus_binom2",
neuper@37974:                      num_str @{thm real_plus_minus_binom2}),   
neuper@37950: 		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37950: 	       (*RL 020915*)
neuper@37969: 	       Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), 
neuper@37950: 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
neuper@37969:                Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), 
neuper@37950: 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
neuper@37969:                Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), 
neuper@37950: 		(*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
neuper@37969:                Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), 
neuper@37950: 		(*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
neuper@37974: 	       Thm ("realpow_multI",num_str @{thm realpow_multI}),
neuper@37950: 		(*(a*b)^^^n = a^^^n * b^^^n*)
neuper@37969: 	       Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
neuper@37950: 	        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
neuper@37974: 	       Thm ("real_minus_binom_pow3",
neuper@37974:                      num_str @{thm real_minus_binom_pow3}),
neuper@37950: 	        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
neuper@37950: 
neuper@37950: 
neuper@37974:               (*Thm ("left_distrib" ,num_str @{thm left_distrib}),	
neuper@37950: 		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	       Thm ("right_distrib",num_str @{thm right_distrib}),	
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37965: 	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),	
neuper@37950: 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
neuper@37982: 	       Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),	
neuper@37950: 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
neuper@37974: 	      *)
neuper@37974: 	       Thm ("mult_1_left",num_str @{thm mult_1_left}),
neuper@37974:                (*"1 * z = z"*)
neuper@37974: 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
neuper@37974:                (*"0 * z = 0"*)
neuper@37965: 	       Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
neuper@37950: 
neuper@38014: 	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Calc ("Atools.pow", eval_binop "#power_"),
neuper@37974:               (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37974: 		(*AC-rewriting*)
neuper@37974: 	       Thm ("real_mult_left_commute",
neuper@37974:                      num_str @{thm real_mult_left_commute}),
neuper@37974: 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
neuper@37974: 	       Thm ("add_commute",num_str @{thm add_commute}),
neuper@37974: 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37974: 	       Thm ("add_assoc",num_str @{thm add_assoc}),
neuper@37974: 	      *)
neuper@37969: 	       Thm ("sym_realpow_twoI",
neuper@37969:                      num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950: 	       (*"r1 * r1 = r1 ^^^ 2"*)
neuper@37969: 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			
neuper@37950: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
neuper@37974: 	       (*Thm ("sym_real_mult_2",
neuper@37974:                        num_str (@{thm real_mult_2} RS @{thm sym})),		
neuper@37950: 	       (*"z1 + z1 = 2 * z1"*)*)
neuper@37969: 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		
neuper@37950: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37950: 
neuper@37969: 	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 
neuper@37974: 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
neuper@37974: 	       Thm ("real_num_collect_assoc",
neuper@37974:                      num_str @{thm real_num_collect_assoc}),	
neuper@37974: 	       (*"[| l is_const; m is_const |] ==>  
neuper@37974:                                        l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37974: 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37974: 	       Thm ("real_one_collect_assoc",
neuper@37974:                      num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37950: 
neuper@38014: 	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Calc ("Atools.pow", eval_binop "#power_")
neuper@37950: 	       ],
neuper@37950:       scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
neuper@37950:       }:rls;      
neuper@37950: 
neuper@37950: 
neuper@37950: (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
neuper@37950: 
neuper@37950: (*FIXME.0401: make SML-order local to make_polynomial(_) *)
neuper@37950: (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
neuper@37950: (* Polynom --> List von Monomen *) 
neuper@38014: fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
neuper@37950:     (poly2list t1) @ (poly2list t2)
neuper@37950:   | poly2list t = [t];
neuper@37950: 
neuper@37950: (* Monom --> Liste von Variablen *)
neuper@37950: fun monom2list (Const ("op *",_) $ t1 $ t2) = 
neuper@37950:     (monom2list t1) @ (monom2list t2)
neuper@37950:   | monom2list t = [t];
neuper@37950: 
neuper@37950: (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
neuper@37950: fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
neuper@37950:   | get_basStr (Free (str, _)) = str
neuper@37950:   | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
neuper@37950: (*| get_basStr t = 
neuper@38031:     error("get_basStr: called with t= "^(term2str t));*)
neuper@37950: 
neuper@37950: (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
neuper@37950: fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
neuper@37950:   | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
neuper@37950:   | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
neuper@37950:   | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
neuper@37950: (*| get_potStr t = 
neuper@38031:     error("get_potStr: called with t= "^(term2str t));*)
neuper@37950: 
neuper@37950: (* Umgekehrte string_ord *)
neuper@37950: val string_ord_rev =  rev_order o string_ord;
neuper@37950: 		
neuper@37950:  (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) 
neuper@37950:     innerhalb eines Monomes:
neuper@37950:     - zuerst lexikographisch nach Variablenname 
neuper@37950:     - wenn gleich: nach steigender Potenz *)
neuper@37950: fun var_ord (a,b: term) = prod_ord string_ord string_ord 
neuper@37950:     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950: 
neuper@37950: (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen); 
neuper@37950:    verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
neuper@37950:    - zuerst lexikographisch nach Variablenname 
neuper@37950:    - wenn gleich: nach sinkender Potenz*)
neuper@37950: fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev 
neuper@37950:     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950: 
neuper@37950: 
neuper@37950: (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
neuper@37950: val sort_varList = sort var_ord;
neuper@37950: 
neuper@37950: (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt 
neuper@37950:    Argumente in eine Liste *)
neuper@37950: fun args u : term list =
neuper@37950:     let fun stripc (f$t, ts) = stripc (f, t::ts)
neuper@37950: 	  | stripc (t as Free _, ts) = (t::ts)
neuper@37950: 	  | stripc (_, ts) = ts
neuper@37950:     in stripc (u, []) end;
neuper@37950:                                     
neuper@37950: (* liefert True, falls der Term (Liste von Termen) nur Zahlen 
neuper@37950:    (keine Variablen) enthaelt *)
neuper@37950: fun filter_num [] = true
neuper@37950:   | filter_num [Free x] = if (is_num (Free x)) then true
neuper@37950: 				else false
neuper@37950:   | filter_num ((Free _)::_) = false
neuper@37950:   | filter_num ts =
neuper@37950:     (filter_num o (filter_out is_num) o flat o (map args)) ts;
neuper@37950: 
neuper@37950: (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt 
neuper@37950:    dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
neuper@37950: fun is_nums t = filter_num [t];
neuper@37950: 
neuper@37950: (* Berechnet den Gesamtgrad eines Monoms *)
neuper@37950: local 
neuper@37950:     fun counter (n, []) = n
neuper@37950:       | counter (n, x :: xs) = 
neuper@37950: 	if (is_nums x) then
neuper@37950: 	    counter (n, xs) 
neuper@37950: 	else 
neuper@37950: 	    (case x of 
neuper@37950: 		 (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) => 
neuper@37950: 		     if (is_nums (Free (str_h, T))) then
neuper@37950: 			 counter (n + (the (int_of_str str_h)), xs)
neuper@37950: 		     else counter (n + 1000, xs) (*FIXME.MG?!*)
neuper@37950: 	       | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => 
neuper@37950: 		     counter (n + 1000, xs) (*FIXME.MG?!*)
neuper@37950: 	       | (Free (str, _)) => counter (n + 1, xs)
neuper@38031: 	     (*| _ => error("monom_degree: called with factor: "^(term2str x)))*)
neuper@37950: 	       | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
neuper@37950: in  
neuper@37950:     fun monom_degree l = counter (0, l) 
neuper@37980: end;(*local*)
neuper@37950: 
neuper@37950: (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich 
neuper@37950:    der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen, 
neuper@37950:    werden jedoch dabei ignoriert (uebersprungen)  *)
neuper@37950: fun dict_cond_ord _ _ ([], []) = EQUAL
neuper@37950:   | dict_cond_ord _ _ ([], _ :: _) = LESS
neuper@37950:   | dict_cond_ord _ _ (_ :: _, []) = GREATER
neuper@37950:   | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
neuper@37950:     (case (cond x, cond y) of 
neuper@37950: 	 (false, false) => (case elem_ord (x, y) of 
neuper@37950: 				EQUAL => dict_cond_ord elem_ord cond (xs, ys) 
neuper@37950: 			      | ord => ord)
neuper@37950:        | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)
neuper@37950:        | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)
neuper@37950:        | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys) );
neuper@37950: 
neuper@37950: (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
neuper@37950:    zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen - 
neuper@37950:    dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
neuper@37950: fun degree_ord (xs, ys) =
neuper@37950: 	    prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums) 
neuper@37950: 	    ((monom_degree xs, xs), (monom_degree ys, ys));
neuper@37950: 
neuper@37950: fun hd_str str = substring (str, 0, 1);
neuper@37950: fun tl_str str = substring (str, 1, (size str) - 1);
neuper@37950: 
neuper@37950: (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
neuper@38031: fun get_koeff_of_mon [] =  error("get_koeff_of_mon: called with l = []")
neuper@37950:   | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
neuper@37950: 				    else NONE;
neuper@37950: 
neuper@37950: (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
neuper@37950: fun koeff2ordStr (SOME x) = (case x of 
neuper@37950: 				 (Free (str, T)) => 
neuper@37950: 				     if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
neuper@37950: 				     else str
neuper@37950: 			       | _ => "aaa") (* "num.Ausdruck" --> gross *)
neuper@37950:   | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
neuper@37950: 
neuper@37950: (* Order zum Vergleich von Koeffizienten (strings): 
neuper@37950:    "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
neuper@37950: fun compare_koeff_ord (xs, ys) = 
neuper@37950:     string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
neuper@37950: 		(koeff2ordStr o get_koeff_of_mon) ys);
neuper@37950: 
neuper@37950: (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
neuper@37950: fun koeff_degree_ord (xs, ys) =
neuper@37950: 	    prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
neuper@37950: 
neuper@37950: (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels 
neuper@37950:    Gesamtgradordnung *)
neuper@37950: val sort_monList = sort koeff_degree_ord;
neuper@37950: 
neuper@37950: (* Alternativ zu degree_ord koennte auch die viel einfachere und 
neuper@37950:    kuerzere Ordnung simple_ord verwendet werden - ist aber nicht 
neuper@37950:    fuer unsere Zwecke geeignet!
neuper@37950: 
neuper@37950: fun simple_ord (al,bl: term list) = dict_ord string_ord 
neuper@37950: 	 (map get_basStr al, map get_basStr bl); 
neuper@37950: 
neuper@37950: val sort_monList = sort simple_ord; *)
neuper@37950: 
neuper@37950: (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt 
neuper@37950:    (mit gewuenschtem Typen T) *)
neuper@38014: fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
neuper@37950: fun mult T = Const ("op *", [T,T] ---> T);
neuper@37950: fun binop op_ t1 t2 = op_ $ t1 $ t2;
neuper@37950: fun create_prod T (a,b) = binop (mult T) a b;
neuper@37950: fun create_sum T (a,b) = binop (plus T) a b;
neuper@37950: 
neuper@37950: (* löscht letztes Element einer Liste *)
neuper@37950: fun drop_last l = take ((length l)-1,l);
neuper@37950: 
neuper@37950: (* Liste von Variablen --> Monom *)
neuper@37950: fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
neuper@37950: (* Bemerkung: 
neuper@37950:    foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei 
neuper@37950:    gleiche Monome zusammengefasst werden können (collect_numerals)! 
neuper@37950:    zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
neuper@37950: 
neuper@37950: (* Liste von Monomen --> Polynom *)	
neuper@37950: fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
neuper@37950: (* Bemerkung: 
neuper@37950:    foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) - 
neuper@37950:    bessere Darstellung, da keine Klammern sichtbar! 
neuper@37950:    (und discard_parentheses in make_polynomial hat weniger zu tun) *)
neuper@37950: 
neuper@37950: (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
neuper@37950: fun sort_variables t = 
neuper@37950:     let
neuper@37950: 	val ll =  map monom2list (poly2list t);
neuper@37950: 	val lls = map sort_varList ll; 
neuper@37950: 	val T = type_of t;
neuper@37950: 	val ls = map (create_monom T) lls;
neuper@37950:     in create_polynom T ls end;
neuper@37950: 
neuper@37950: (* sorts the monoms of an expanded and variable-sorted polynomial 
neuper@37950:    by total_degree *)
neuper@37950: fun sort_monoms t = 
neuper@37950:     let
neuper@37950: 	val ll =  map monom2list (poly2list t);
neuper@37950: 	val lls = sort_monList ll;
neuper@37950: 	val T = type_of t;
neuper@37950: 	val ls = map (create_monom T) lls;
neuper@37950:     in create_polynom T ls end;
neuper@37950: 
neuper@37950: (* auch Klammerung muss übereinstimmen; 
neuper@37950:    sort_variables klammert Produkte rechtslastig*)
neuper@37950: fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
neuper@37950: 
neuper@37950: fun eval_is_multUnordered (thmid:string) _ 
neuper@37950: 		       (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy = 
neuper@37950:     if is_multUnordered arg
neuper@37950:     then SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950:     else SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950:   | eval_is_multUnordered _ _ _ _ = NONE; 
neuper@37950: 
neuper@37950: 
neuper@37950: fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
neuper@37950:     []:(rule * (term * term list)) list;
neuper@37950: fun init_state (_:term) = e_rrlsstate;
neuper@37950: fun locate_rule (_:rule list list) (_:term) (_:rule) =
neuper@37950:     ([]:(rule * (term * term list)) list);
neuper@37950: fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
neuper@37950: fun normal_form t = SOME (sort_variables t,[]:term list);
neuper@37950: 
neuper@37950: val order_mult_ =
neuper@37950:     Rrls {id = "order_mult_", 
neuper@37950: 	  prepat = 
neuper@37950: 	  [([(term_of o the o (parse thy)) "p is_multUnordered"], 
neuper@37976: 	    parse_patt thy "?p" )],
neuper@37950: 	  rew_ord = ("dummy_ord", dummy_ord),
neuper@37950: 	  erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
neuper@37976: 			    [Calc ("Poly.is'_multUnordered", 
neuper@37976:                                     eval_is_multUnordered "")],
neuper@38014: 	  calc = [("PLUS"  , ("Groups.plus_class.plus"      , eval_binop "#add_")),
neuper@37976: 		  ("TIMES" , ("op *"      , eval_binop "#mult_")),
neuper@38014: 		  ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
neuper@37976: 		  ("POWER" , ("Atools.pow", eval_binop "#power_"))],
neuper@37950: 	  scr=Rfuns {init_state  = init_state,
neuper@37950: 		     normal_form = normal_form,
neuper@37950: 		     locate_rule = locate_rule,
neuper@37950: 		     next_rule   = next_rule,
neuper@37950: 		     attach_form = attach_form}};
neuper@37950: val order_mult_rls_ = 
neuper@37950:   Rls{id = "order_mult_rls_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       rules = [Rls_ order_mult_
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
neuper@37950: 
neuper@37950: (*WN.18.6.03 *)
neuper@37950: (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
neuper@37950: fun eval_is_addUnordered (thmid:string) _ 
neuper@37950: 		       (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy = 
neuper@37950:     if is_addUnordered arg
neuper@37950:     then SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950:     else SOME (mk_thmid thmid "" 
neuper@37950: 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 
neuper@37950: 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950:   | eval_is_addUnordered _ _ _ _ = NONE; 
neuper@37950: 
neuper@37950: fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
neuper@37950:     []:(rule * (term * term list)) list;
neuper@37950: fun init_state (_:term) = e_rrlsstate;
neuper@37950: fun locate_rule (_:rule list list) (_:term) (_:rule) =
neuper@37950:     ([]:(rule * (term * term list)) list);
neuper@37950: fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
neuper@37950: fun normal_form t = SOME (sort_monoms t,[]:term list);
neuper@37950: 
neuper@37950: val order_add_ =
neuper@37950:     Rrls {id = "order_add_", 
neuper@37950: 	  prepat = (*WN.18.6.03 Preconditions und Pattern,
neuper@37950: 		    die beide passen muessen, damit das Rrls angewandt wird*)
neuper@37950: 	  [([(term_of o the o (parse thy)) "p is_addUnordered"], 
neuper@37976: 	    parse_patt thy "?p" 
neuper@37950: 	    (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment 
neuper@37950: 	      fuer die Evaluation der Precondition "p is_addUnordered"*))],
neuper@37950: 	  rew_ord = ("dummy_ord", dummy_ord),
neuper@37950: 	  erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
neuper@37950: 			    [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
neuper@37972: 			     (*WN.18.6.03 definiert in thy,
neuper@37950:                                evaluiert prepat*)],
neuper@38014: 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
neuper@37950: 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
neuper@38014: 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
neuper@37950: 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
neuper@37950: 	  (*asm_thm=[],*)
neuper@37950: 	  scr=Rfuns {init_state  = init_state,
neuper@37950: 		     normal_form = normal_form,
neuper@37950: 		     locate_rule = locate_rule,
neuper@37950: 		     next_rule   = next_rule,
neuper@37950: 		     attach_form = attach_form}};
neuper@37950: 
neuper@37950: val order_add_rls_ = 
neuper@37950:   Rls{id = "order_add_rls_", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = e_rls,srls = Erls,
neuper@37950:       calc = [],
neuper@37950:       (*asm_thm = [],*)
neuper@37950:       rules = [Rls_ order_add_
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: (*. see MG-DA.p.52ff .*)
neuper@37950: val make_polynomial(*MG.03, overwrites version from above, 
neuper@37950:     previously 'make_polynomial_'*) =
neuper@37950:   Seq {id = "make_polynomial", preconds = []:term list, 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls, srls = Erls,calc = [],
neuper@37980:       rules = [Rls_ discard_minus,
neuper@37950: 	       Rls_ expand_poly_,
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Rls_ order_mult_rls_,
neuper@37950: 	       Rls_ simplify_power_, 
neuper@37950: 	       Rls_ calc_add_mult_pow_, 
neuper@37950: 	       Rls_ reduce_012_mult_,
neuper@37950: 	       Rls_ order_add_rls_,
neuper@37950: 	       Rls_ collect_numerals_, 
neuper@37950: 	       Rls_ reduce_012_,
neuper@37979: 	       Rls_ discard_parentheses1
neuper@37950: 	       ],
neuper@37950:       scr = EmptyScr
neuper@37950:       }:rls;
neuper@37950: val norm_Poly(*=make_polynomial*) = 
neuper@37950:   Seq {id = "norm_Poly", preconds = []:term list, 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls, srls = Erls, calc = [],
neuper@37980:       rules = [Rls_ discard_minus,
neuper@37950: 	       Rls_ expand_poly_,
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Rls_ order_mult_rls_,
neuper@37950: 	       Rls_ simplify_power_, 
neuper@37950: 	       Rls_ calc_add_mult_pow_, 
neuper@37950: 	       Rls_ reduce_012_mult_,
neuper@37950: 	       Rls_ order_add_rls_,
neuper@37950: 	       Rls_ collect_numerals_, 
neuper@37950: 	       Rls_ reduce_012_,
neuper@37979: 	       Rls_ discard_parentheses1
neuper@37950: 	       ],
neuper@37950:       scr = EmptyScr
neuper@37950:       }:rls;
neuper@37950: 
neuper@37979: (* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses1 
neuper@37950:    and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
neuper@37950: (* MG necessary  for termination of norm_Rational(*_mg*) in Rational.ML*)
neuper@37950: val make_rat_poly_with_parentheses =
neuper@37950:   Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list, 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord),
neuper@37950:       erls = Atools_erls, srls = Erls, calc = [],
neuper@37980:       rules = [Rls_ discard_minus,
neuper@37950: 	       Rls_ expand_poly_rat_,(*ignors rationals*)
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	       Rls_ order_mult_rls_,
neuper@37950: 	       Rls_ simplify_power_, 
neuper@37950: 	       Rls_ calc_add_mult_pow_, 
neuper@37950: 	       Rls_ reduce_012_mult_,
neuper@37950: 	       Rls_ order_add_rls_,
neuper@37950: 	       Rls_ collect_numerals_, 
neuper@37950: 	       Rls_ reduce_012_
neuper@37979: 	       (*Rls_ discard_parentheses1 *)
neuper@37950: 	       ],
neuper@37950:       scr = EmptyScr
neuper@37950:       }:rls;
neuper@37950: 
neuper@37950: (*.a minimal ruleset for reverse rewriting of factions [2];
neuper@37950:    compare expand_binoms.*)
neuper@37950: val rev_rew_p = 
neuper@37950: Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
neuper@37950:     erls = Atools_erls, srls = Erls,
neuper@38014:     calc = [(*("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@37950: 	    ("TIMES" , ("op *", eval_binop "#mult_")),
neuper@37950: 	    ("POWER", ("Atools.pow", eval_binop "#power_"))*)
neuper@37950: 	    ],
neuper@37969:     rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
neuper@37950: 	     (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
neuper@37969: 	     Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}),
neuper@37950: 	     (*"(a +  1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
neuper@37969: 	     Thm ("real_plus_binom_times2" ,num_str @{thm real_plus_binom_times2}),
neuper@37950: 	     (*"(a + -1*b)*(a +  1*b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 
neuper@37965: 	     Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
neuper@37950: 
neuper@37965:              Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950: 	     (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37974: 	     Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950: 	     (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
neuper@37969: 	     Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}),
neuper@37950: 	     (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
neuper@37950: 	     Rls_ order_mult_rls_,
neuper@37950: 	     (*Rls_ order_add_rls_,*)
neuper@37950: 
neuper@38014: 	     Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
neuper@37950: 	     Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	     Calc ("Atools.pow", eval_binop "#power_"),
neuper@37950: 	     
neuper@37969: 	     Thm ("sym_realpow_twoI",
neuper@37969:                    num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950: 	     (*"r1 * r1 = r1 ^^^ 2"*)
neuper@37969: 	     Thm ("sym_real_mult_2",
neuper@37969:                    num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950: 	     (*"z1 + z1 = 2 * z1"*)
neuper@37969: 	     Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
neuper@37950: 	     (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37950: 
neuper@37969: 	     Thm ("real_num_collect",num_str @{thm real_num_collect}), 
neuper@37950: 	     (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37969: 	     Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950: 	     (*"[| l is_const; m is_const |] ==>  
neuper@37950:                                      l * n + (m * n + k) =  (l + m) * n + k"*)
neuper@37969: 	     Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950: 	     (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37969: 	     Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	     (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37950: 
neuper@37969: 	     Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950: 	     (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950: 
neuper@38014: 	     Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
neuper@37950: 	     Calc ("op *", eval_binop "#mult_"),
neuper@37950: 	     Calc ("Atools.pow", eval_binop "#power_"),
neuper@37950: 
neuper@37965: 	     Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
neuper@37965: 	     Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
neuper@37965: 	     Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*)
neuper@37950: 
neuper@37950: 	     (*Rls_ order_add_rls_*)
neuper@37950: 	     ],
neuper@37950: 
neuper@37950:     scr = EmptyScr}:rls;      
neuper@37950: 
neuper@37950: ruleset' := 
neuper@37967: overwritelthy @{theory} (!ruleset',
neuper@37950: 		   [("norm_Poly", prep_rls norm_Poly),
neuper@37950: 		    ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
neuper@37950: 		    ("expand", prep_rls expand),
neuper@37950: 		    ("expand_poly", prep_rls expand_poly),
neuper@37950: 		    ("simplify_power", prep_rls simplify_power),
neuper@37950: 		    ("order_add_mult", prep_rls order_add_mult),
neuper@37950: 		    ("collect_numerals", prep_rls collect_numerals),
neuper@37950: 		    ("collect_numerals_", prep_rls collect_numerals_),
neuper@37950: 		    ("reduce_012", prep_rls reduce_012),
neuper@37950: 		    ("discard_parentheses", prep_rls discard_parentheses),
neuper@37950: 		    ("make_polynomial", prep_rls make_polynomial),
neuper@37950: 		    ("expand_binoms", prep_rls expand_binoms),
neuper@37950: 		    ("rev_rew_p", prep_rls rev_rew_p),
neuper@37980: 		    ("discard_minus", prep_rls discard_minus),
neuper@37950: 		    ("expand_poly_", prep_rls expand_poly_),
neuper@37950: 		    ("expand_poly_rat_", prep_rls expand_poly_rat_),
neuper@37950: 		    ("simplify_power_", prep_rls simplify_power_),
neuper@37950: 		    ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
neuper@37950: 		    ("reduce_012_mult_", prep_rls reduce_012_mult_),
neuper@37950: 		    ("reduce_012_", prep_rls reduce_012_),
neuper@37979: 		    ("discard_parentheses1",prep_rls discard_parentheses1),
neuper@37950: 		    ("order_mult_rls_", prep_rls order_mult_rls_),
neuper@37950: 		    ("order_add_rls_", prep_rls order_add_rls_),
neuper@37950: 		    ("make_rat_poly_with_parentheses", 
neuper@37950: 		     prep_rls make_rat_poly_with_parentheses)
neuper@37950: 		    ]);
neuper@37950: 
neuper@37950: calclist':= overwritel (!calclist', 
neuper@37950:    [("is_polyrat_in", ("Poly.is'_polyrat'_in", 
neuper@37950: 		       eval_is_polyrat_in "#eval_is_polyrat_in")),
neuper@37950:     ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
neuper@37950:     ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
neuper@37950:     ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
neuper@37950:     ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
neuper@37950:     ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
neuper@37950:     ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
neuper@37950:     ]);
neuper@37950: 
neuper@37976: val ------------------------------------------------------ = "11111";
neuper@37950: 
neuper@37950: (** problems **)
neuper@37950: 
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_simp_poly" [] e_pblID
neuper@37950:  (["polynomial","simplification"],
neuper@37976:   [("#Given" ,["TERM t_t"]),
neuper@37976:    ("#Where" ,["t_t is_polyexp"]),
neuper@37976:    ("#Find"  ,["normalform n_n"])
neuper@37950:   ],
neuper@37950:   append_rls "e_rls" e_rls [(*for preds in where_*)
neuper@37950: 			    Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
neuper@37976:   SOME "Simplify t_t", 
neuper@37950:   [["simplification","for_polynomials"]]));
neuper@37950: 
neuper@37950: (** methods **)
neuper@37950: 
neuper@37950: store_met
neuper@37972:     (prep_met thy "met_simp_poly" [] e_metID
neuper@37950: 	      (["simplification","for_polynomials"],
neuper@37976: 	       [("#Given" ,["TERM t_t"]),
neuper@37976: 		("#Where" ,["t_t is_polyexp"]),
neuper@37976: 		("#Find"  ,["normalform n_n"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true",
neuper@37950: 		rls' = e_rls,
neuper@37950: 		calc = [], 
neuper@37950: 		srls = e_rls, 
neuper@37950: 		prls = append_rls "simplification_for_polynomials_prls" e_rls 
neuper@37950: 				  [(*for preds in where_*)
neuper@37950: 				   Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
neuper@37950: 		crls = e_rls, nrls = norm_Poly},
neuper@37976: 	       "Script SimplifyScript (t_t::real) =                " ^
neuper@37976: 	       "  ((Rewrite_Set norm_Poly False) t_t)"
neuper@37950: 	       ));
neuper@37950: *}
neuper@37950: 
neuper@37906: end




