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: 
wneuper@59523: subsection \<open>remark on term-structure of polynomials\<close>
wneuper@59523: text \<open>
wneuper@59523: WN190319:
wneuper@59523: the code below reflects missing coordination between two authors:
wneuper@59523: * ML: built the equation solver; simple rule-sets, programs; better predicates for specifications.
wneuper@59523: * MG: built simplification of polynomials with AC rewriting by ML code
wneuper@59523: 
wneuper@59523: WN020919:
wneuper@59523: *** there are 5 kinds of expanded normalforms ***
wneuper@59523: 
wneuper@59523: [1] 'complete polynomial' (Komplettes Polynom), univariate
wneuper@59523:    a_0 + a_1.x^1 +...+ a_n.x^n   not (a_n = 0)
wneuper@59523: 	        not (a_n = 0), some a_i may be zero (DON'T disappear),
wneuper@59523:                 variables in monomials lexicographically ordered and complete,
wneuper@59523:                 x written as 1*x^1, ...
wneuper@59523: [2] 'polynomial' (Polynom), univariate and multivariate
wneuper@59523:    a_0 + a_1.x +...+ a_n.x^n   not (a_n = 0)
wneuper@59523:    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
wneuper@59523: 	        not (a_n = 0), some a_i may be zero (ie. monomials disappear),
wneuper@59523:                 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
wneuper@59523:                 and variables in monomials are lexicographically ordered  
wneuper@59523:    examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
wneuper@59523: 	     [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
wneuper@59523: 	     [2]: "x + (-50) * x ^^^ 3"
wneuper@59523: 	     [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
wneuper@59523: 
wneuper@59523: [3] 'expanded_term' (Ausmultiplizierter Term):
wneuper@59523:    pull out unary minus to binary minus, 
wneuper@59523:    as frequently exercised in schools; other conditions for [2] hold however
wneuper@59523:    examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
wneuper@59523: 	     "4 * x ^^^ 2 - 9 * y ^^^ 2"
wneuper@59523: [4] 'polynomial_in' (Polynom in): 
wneuper@59523:    polynomial in 1 variable with arbitrary coefficients
wneuper@59523:    examples: "2 * x + (-50) * x ^^^ 3"                     (poly in x)
wneuper@59523: 	     "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
wneuper@59523: [5] 'expanded_in' (Ausmultiplizierter Termin in): 
wneuper@59523:    analoguous to [3] with binary minus like [3]
wneuper@59523:    examples: "2 * x - 50 * x ^^^ 3"                     (expanded in x)
wneuper@59523: 	     "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
wneuper@59523: \<close>
wneuper@59523: subsection \<open>consts definition for predicates in specifications\<close>
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: 
wneuper@59523: subsection \<open>theorems not yet adopted from Isabelle\<close>
neuper@52148: axiomatization where (*.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@52148:   realpow_pow:             "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
neuper@52148:   realpow_addI:            "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
neuper@52148:   realpow_addI_assoc_l:    "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
neuper@52148:   realpow_addI_assoc_r:    "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
neuper@37906: 		  
neuper@52148:   realpow_oneI:            "r ^^^ 1 = r" and
neuper@52148:   realpow_zeroI:            "r ^^^ 0 = 1" and
neuper@52148:   realpow_eq_oneI:         "1 ^^^ n = 1" and
neuper@52148:   realpow_multI:           "(r * s) ^^^ n = r ^^^ n * s ^^^ n"  and
neuper@37974:   realpow_multI_poly:      "[| r is_polyexp; s is_polyexp |] ==>
neuper@52148: 			      (r * s) ^^^ n = r ^^^ n * s ^^^ n"  and
wneuper@59189:   realpow_minus_oneI:      "(- 1) ^^^ (2 * n) = 1"  and 
wneuper@59589:   real_diff_0:		         "0 - x = - (x::real)" and
neuper@37906: 
neuper@52148:   realpow_twoI:            "r ^^^ 2 = r * r" and
neuper@52148:   realpow_twoI_assoc_l:	  "r * (r * s) = r ^^^ 2 * s" and
neuper@52148:   realpow_twoI_assoc_r:	  "s * r * r = s * r ^^^ 2" and
neuper@52148:   realpow_two_atom:        "r is_atom ==> r * r = r ^^^ 2" and
neuper@52148:   realpow_plus_1:          "r * r ^^^ n = r ^^^ (n + 1)"   and       
neuper@52148:   realpow_plus_1_assoc_l:  "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"  and
neuper@52148:   realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"  and
neuper@52148:   realpow_plus_1_assoc_r:  "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
neuper@52148:   realpow_plus_1_atom:     "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
neuper@37974:   realpow_def_atom:        "[| Not (r is_atom); 1 < n |]
neuper@52148: 			   ==> r ^^^ n = r * r ^^^ (n + -1)" and
neuper@52148:   realpow_addI_atom:       "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
neuper@37906: 
neuper@37906: 
neuper@52148:   realpow_minus_even:	  "n is_even ==> (- r) ^^^ n = r ^^^ n" and
neuper@52148:   realpow_minus_odd:       "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
neuper@37906: 
neuper@37906: 
neuper@37906: (* RL 020914 *)
neuper@52148:   real_pp_binom_times:     "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
neuper@52148:   real_pm_binom_times:     "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
neuper@52148:   real_mp_binom_times:     "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
neuper@52148:   real_mm_binom_times:     "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
neuper@52148:   real_plus_binom_pow3:    "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
neuper@37974:   real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==> 
neuper@52148: 			    (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
neuper@52148:   real_minus_binom_pow3:   "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
neuper@37974:   real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
neuper@52148:                            -1*b^^^3" and
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@52148:                            *(a + b)" and
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@52148:                            *(a + b)" and
neuper@37974:   real_plus_binom_pow5:    "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
neuper@52148:                            *(a^^^2 + 2*a*b + b^^^2)" and
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@52148:                                 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
neuper@52148:   real_diff_plus:          "a - b = a + -b" (*17.3.03: do_NOT_use*) and
neuper@52148:   real_diff_minus:         "a - b = a + -1 * b" and
neuper@52148:   real_plus_binom_times:   "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
neuper@52148:   real_minus_binom_times:  "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
neuper@37906:   (*WN071229 changed for Schaerding -----vvv*)
neuper@37974:   (*real_plus_binom_pow2:  "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
neuper@52148:   real_plus_binom_pow2:    "(a + b)^^^2 = (a + b) * (a + b)" and
neuper@37906:   (*WN071229 changed for Schaerding -----^^^*)
neuper@37974:   real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
neuper@52148: 			       (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
neuper@52148:   real_minus_binom_pow2:      "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
neuper@52148:   real_minus_binom_pow2_p:    "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
neuper@52148:   real_plus_minus_binom1:     "(a + b)*(a - b) = a^^^2 - b^^^2" and
neuper@52148:   real_plus_minus_binom1_p:   "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
neuper@52148:   real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
neuper@52148:   real_plus_minus_binom2:     "(a - b)*(a + b) = a^^^2 - b^^^2" and
neuper@52148:   real_plus_minus_binom2_p:   "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
neuper@52148:   real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
neuper@52148:   real_plus_binom_times1:     "(a +  1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
neuper@52148:   real_plus_binom_times2:     "(a + -1*b)*(a +  1*b) = a^^^2 + -1*b^^^2" and
neuper@37906: 
neuper@37974:   real_num_collect:           "[| l is_const; m is_const |] ==>
neuper@52148: 			      l * n + m * n = (l + m) * n" and
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@52148: 			      l * n + (m * n + k) = (l + m) * n + k" and
neuper@37974:   real_num_collect_assoc_l:   "[| l is_const; m is_const |] ==>
neuper@37950: 			      l * n + (m * n + k) = (l + m)
neuper@52148: 				* n + k" and
neuper@37974:   real_num_collect_assoc_r:   "[| l is_const; m is_const |] ==>
neuper@52148: 			      (k + m * n) + l * n = k + (l + m) * n" and
neuper@52148:   real_one_collect:           "m is_const ==> n + m * n = (1 + m) * n" and
neuper@37906: (* FIXME.MG.0401: replace 'real_one_collect_assoc' 
neuper@37906: 	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
neuper@52148:   real_one_collect_assoc:     "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
neuper@37906: 
neuper@52148:   real_one_collect_assoc_l:   "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
neuper@52148:   real_one_collect_assoc_r:  "m is_const ==> (k + n) +  m * n = k + (1 + m) * n" and
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@52148:   real_mult_2_assoc:          "z1 + (z1 + k) = 2 * z1 + k" and
neuper@52148:   real_mult_2_assoc_l:        "z1 + (z1 + k) = 2 * z1 + k" and
neuper@52148:   real_mult_2_assoc_r:        "(k + z1) + z1 = k + 2 * z1" and
neuper@37906: 
wneuper@59587:   real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and
wneuper@59587:   real_mult_minus1:       "-1 * z = - (z::real)" and
wneuper@59587:   real_mult_2:            "2 * z = z + (z::real)" and
wneuper@59587: 
neuper@52148:   real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
neuper@37974:   real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
neuper@37950: 
wneuper@59523: subsection \<open>auxiliary functions\<close>
wneuper@59530: ML \<open>
wneuper@59530: val thy = @{theory};
wneuper@59530: val poly_consts =
wneuper@59530:   ["Groups.plus_class.plus", "Groups.minus_class.minus",
wneuper@59531:   "Rings.divide_class.divide", "Groups.times_class.times",
walther@59603:   "Prog_Expr.pow"];
wneuper@59530: \<close>
wneuper@59523: subsubsection \<open>for predicates in specifications (ML)\<close>
wneuper@59472: ML \<open>
wneuper@59522: (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
wneuper@59522: (*. a 'monomial t in variable v' is a term t with
wneuper@59522:   either (1) v NOT existent in t, or (2) v contained in t,
wneuper@59522:   if (1) then degree 0
wneuper@59522:   if (2) then v is a factor on the very right, ev. with exponent.*)
wneuper@59522: fun factor_right_deg (*case 2*)
walther@59603: 	    (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Prog_Expr.pow",_) $ vv $ Free (d, _))) v =
walther@59603: 	   if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
walther@59603:   | factor_right_deg (Const ("Prog_Expr.pow",_) $ vv $ Free (d,_)) v =
wneuper@59522: 	   if (vv = v) then SOME (TermC.int_of_str d) else NONE
wneuper@59522:   | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v = 
walther@59603: 	   if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
wneuper@59522:   | factor_right_deg vv v =
wneuper@59522: 	  if (vv = v) then SOME 1 else NONE;    
wneuper@59522: fun mono_deg_in m v =  (*case 1*)
walther@59603: 	if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
wneuper@59522: 
wneuper@59522: fun expand_deg_in t v =
wneuper@59522: 	let
wneuper@59522:     fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) =
wneuper@59522:           (case mono_deg_in t2 v of (* $ is left associative*)
wneuper@59522:             SOME d' => edi d' d' t1 | NONE => NONE)
wneuper@59522:       | edi ~1 ~1 (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
wneuper@59522:           (case mono_deg_in t2 v of
wneuper@59522:             SOME d' => edi d' d' t1 | NONE => NONE)
wneuper@59522:       | edi d dmax (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
wneuper@59522:           (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)
wneuper@59522: 	        SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
wneuper@59522:           | NONE => NONE)
wneuper@59522:       | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
wneuper@59522:           (case mono_deg_in t2 v of
wneuper@59522:             SOME d' =>    (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)
wneuper@59522:               if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
wneuper@59522:           | NONE => NONE)
wneuper@59522:       | edi ~1 ~1 t =
wneuper@59522:           (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)
wneuper@59522:       | edi d dmax t = (*basecase last*)
wneuper@59522:     	    (case mono_deg_in t v of
wneuper@59522:     	      SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
wneuper@59522: 		      | NONE => NONE)
wneuper@59522: 	in edi ~1 ~1 t end;
wneuper@59522: 
wneuper@59522: fun poly_deg_in t v =
wneuper@59522: 	let
wneuper@59522:     fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
wneuper@59522: 		    (case mono_deg_in t2 v of (* $ is left associative *)
wneuper@59522: 		      SOME d' => edi d' d' t1
wneuper@59522:         | NONE => NONE)
wneuper@59522: 	    | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
wneuper@59522: 		    (case mono_deg_in t2 v of
wneuper@59522: 	        SOME d' =>    (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)
wneuper@59522:             if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
wneuper@59522:         | NONE => NONE)
wneuper@59522: 	    | edi ~1 ~1 t =
wneuper@59522:         (case mono_deg_in t v of
wneuper@59522: 		      d as SOME _ => d
wneuper@59522:         | NONE => NONE)
wneuper@59522: 	    | edi d dmax t = (* basecase last *)
wneuper@59522: 		    (case mono_deg_in t v of
wneuper@59522: 		      SOME d' =>
wneuper@59522:             if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
wneuper@59522:         | NONE => NONE)
wneuper@59522: 	in edi ~1 ~1 t end;
wneuper@59523: \<close>
neuper@37950: 
wneuper@59523: subsubsection \<open>for hard-coded AC rewriting (MG)\<close>
wneuper@59523: ML \<open>
wneuper@59523: (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
neuper@37950: 
wneuper@59523: (*FIXME.0401: make SML-order local to make_polynomial(_) *)
wneuper@59523: (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
wneuper@59523: (* Polynom --> List von Monomen *) 
wneuper@59523: fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
wneuper@59523:     (poly2list t1) @ (poly2list t2)
wneuper@59523:   | poly2list t = [t];
neuper@37950: 
wneuper@59523: (* Monom --> Liste von Variablen *)
wneuper@59523: fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) = 
wneuper@59523:     (monom2list t1) @ (monom2list t2)
wneuper@59523:   | monom2list t = [t];
neuper@37950: 
wneuper@59523: (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
walther@59603: fun get_basStr (Const ("Prog_Expr.pow",_) $ Free (str, _) $ _) = str
wneuper@59523:   | get_basStr (Free (str, _)) = str
wneuper@59523:   | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
wneuper@59523: (*| get_basStr t = 
wneuper@59523:     error("get_basStr: called with t= "^(Rule.term2str t));*)
neuper@37950: 
wneuper@59523: (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
walther@59603: fun get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ Free (str, _)) = str
walther@59603:   | get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
wneuper@59523:   | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
wneuper@59523:   | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
wneuper@59523: (*| get_potStr t = 
wneuper@59523:     error("get_potStr: called with t= "^(Rule.term2str t));*)
neuper@37978: 
wneuper@59523: (* Umgekehrte string_ord *)
wneuper@59523: val string_ord_rev =  rev_order o string_ord;
wneuper@59523: 		
wneuper@59523:  (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) 
wneuper@59523:     innerhalb eines Monomes:
wneuper@59523:     - zuerst lexikographisch nach Variablenname 
wneuper@59523:     - wenn gleich: nach steigender Potenz *)
wneuper@59523: fun var_ord (a,b: term) = prod_ord string_ord string_ord 
wneuper@59523:     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950: 
wneuper@59523: (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen); 
wneuper@59523:    verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
wneuper@59523:    - zuerst lexikographisch nach Variablenname 
wneuper@59523:    - wenn gleich: nach sinkender Potenz*)
wneuper@59523: fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev 
wneuper@59523:     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950: 
wneuper@59523: 
wneuper@59523: (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
wneuper@59523: val sort_varList = sort var_ord;
wneuper@59523: 
wneuper@59523: (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt 
wneuper@59523:    Argumente in eine Liste *)
wneuper@59523: fun args u : term list =
wneuper@59523:     let fun stripc (f$t, ts) = stripc (f, t::ts)
wneuper@59523: 	  | stripc (t as Free _, ts) = (t::ts)
wneuper@59523: 	  | stripc (_, ts) = ts
wneuper@59523:     in stripc (u, []) end;
wneuper@59523:                                     
wneuper@59523: (* liefert True, falls der Term (Liste von Termen) nur Zahlen 
wneuper@59523:    (keine Variablen) enthaelt *)
wneuper@59523: fun filter_num [] = true
wneuper@59523:   | filter_num [Free x] = if (TermC.is_num (Free x)) then true
wneuper@59523: 				else false
wneuper@59523:   | filter_num ((Free _)::_) = false
wneuper@59523:   | filter_num ts =
wneuper@59523:     (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
wneuper@59523: 
wneuper@59523: (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt 
wneuper@59523:    dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
wneuper@59523: fun is_nums t = filter_num [t];
wneuper@59523: 
wneuper@59523: (* Berechnet den Gesamtgrad eines Monoms *)
wneuper@59523: local 
wneuper@59523:     fun counter (n, []) = n
wneuper@59523:       | counter (n, x :: xs) = 
wneuper@59523: 	if (is_nums x) then
wneuper@59523: 	    counter (n, xs) 
wneuper@59523: 	else 
wneuper@59523: 	    (case x of 
walther@59603: 		 (Const ("Prog_Expr.pow", _) $ Free _ $ Free (str_h, T)) => 
wneuper@59523: 		     if (is_nums (Free (str_h, T))) then
wneuper@59523: 			 counter (n + (the (TermC.int_of_str_opt str_h)), xs)
wneuper@59523: 		     else counter (n + 1000, xs) (*FIXME.MG?!*)
walther@59603: 	       | (Const ("Prog_Expr.pow", _) $ Free _ $ _ ) => 
wneuper@59523: 		     counter (n + 1000, xs) (*FIXME.MG?!*)
wneuper@59523: 	       | (Free _) => counter (n + 1, xs)
wneuper@59523: 	     (*| _ => error("monom_degree: called with factor: "^(Rule.term2str x)))*)
wneuper@59523: 	       | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
wneuper@59523: in  
wneuper@59523:     fun monom_degree l = counter (0, l) 
wneuper@59523: end;(*local*)
wneuper@59523: 
wneuper@59523: (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich 
wneuper@59523:    der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen, 
wneuper@59523:    werden jedoch dabei ignoriert (uebersprungen)  *)
wneuper@59523: fun dict_cond_ord _ _ ([], []) = EQUAL
wneuper@59523:   | dict_cond_ord _ _ ([], _ :: _) = LESS
wneuper@59523:   | dict_cond_ord _ _ (_ :: _, []) = GREATER
wneuper@59523:   | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
wneuper@59523:     (case (cond x, cond y) of 
wneuper@59523: 	 (false, false) => (case elem_ord (x, y) of 
wneuper@59523: 				EQUAL => dict_cond_ord elem_ord cond (xs, ys) 
wneuper@59523: 			      | ord => ord)
wneuper@59523:        | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)
wneuper@59523:        | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)
wneuper@59523:        | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys) );
wneuper@59523: 
wneuper@59523: (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
wneuper@59523:    zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen - 
wneuper@59523:    dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
wneuper@59523: fun degree_ord (xs, ys) =
wneuper@59523: 	    prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums) 
wneuper@59523: 	    ((monom_degree xs, xs), (monom_degree ys, ys));
wneuper@59523: 
wneuper@59523: fun hd_str str = substring (str, 0, 1);
wneuper@59523: fun tl_str str = substring (str, 1, (size str) - 1);
wneuper@59523: 
wneuper@59523: (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
wneuper@59523: fun get_koeff_of_mon [] =  error("get_koeff_of_mon: called with l = []")
wneuper@59523:   | get_koeff_of_mon (x::_) = if is_nums x then SOME x else NONE;
wneuper@59523: 
wneuper@59523: (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
wneuper@59523: fun koeff2ordStr (SOME x) = (case x of 
wneuper@59523: 				 (Free (str, _)) => 
wneuper@59523: 				     if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
wneuper@59523: 				     else str
wneuper@59523: 			       | _ => "aaa") (* "num.Ausdruck" --> gross *)
wneuper@59523:   | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
wneuper@59523: 
wneuper@59523: (* Order zum Vergleich von Koeffizienten (strings): 
wneuper@59523:    "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
wneuper@59523: fun compare_koeff_ord (xs, ys) = 
wneuper@59523:     string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
wneuper@59523: 		(koeff2ordStr o get_koeff_of_mon) ys);
wneuper@59523: 
wneuper@59523: (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
wneuper@59523: fun koeff_degree_ord (xs, ys) =
wneuper@59523: 	    prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
wneuper@59523: 
wneuper@59523: (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels 
wneuper@59523:    Gesamtgradordnung *)
wneuper@59523: val sort_monList = sort koeff_degree_ord;
wneuper@59523: 
wneuper@59523: (* Alternativ zu degree_ord koennte auch die viel einfachere und 
wneuper@59523:    kuerzere Ordnung simple_ord verwendet werden - ist aber nicht 
wneuper@59523:    fuer unsere Zwecke geeignet!
wneuper@59523: 
wneuper@59523: fun simple_ord (al,bl: term list) = dict_ord string_ord 
wneuper@59523: 	 (map get_basStr al, map get_basStr bl); 
wneuper@59523: 
wneuper@59523: val sort_monList = sort simple_ord; *)
wneuper@59523: 
wneuper@59523: (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt 
wneuper@59523:    (mit gewuenschtem Typen T) *)
wneuper@59523: fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
wneuper@59523: fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
wneuper@59523: fun binop op_ t1 t2 = op_ $ t1 $ t2;
wneuper@59523: fun create_prod T (a,b) = binop (mult T) a b;
wneuper@59523: fun create_sum T (a,b) = binop (plus T) a b;
wneuper@59523: 
wneuper@59523: (* löscht letztes Element einer Liste *)
wneuper@59523: fun drop_last l = take ((length l)-1,l);
wneuper@59523: 
wneuper@59523: (* Liste von Variablen --> Monom *)
wneuper@59523: fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
wneuper@59523: (* Bemerkung: 
wneuper@59523:    foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei 
wneuper@59523:    gleiche Monome zusammengefasst werden können (collect_numerals)! 
wneuper@59523:    zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
wneuper@59523: 
wneuper@59523: (* Liste von Monomen --> Polynom *)	
wneuper@59523: fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
wneuper@59523: (* Bemerkung: 
wneuper@59523:    foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) - 
wneuper@59523:    bessere Darstellung, da keine Klammern sichtbar! 
wneuper@59523:    (und discard_parentheses in make_polynomial hat weniger zu tun) *)
wneuper@59523: 
wneuper@59523: (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
wneuper@59523: fun sort_variables t = 
wneuper@59523:     let
wneuper@59523: 	val ll =  map monom2list (poly2list t);
wneuper@59523: 	val lls = map sort_varList ll; 
wneuper@59523: 	val T = type_of t;
wneuper@59523: 	val ls = map (create_monom T) lls;
wneuper@59523:     in create_polynom T ls end;
wneuper@59523: 
wneuper@59523: (* sorts the monoms of an expanded and variable-sorted polynomial 
wneuper@59523:    by total_degree *)
wneuper@59523: fun sort_monoms t = 
wneuper@59523:     let
wneuper@59523: 	val ll =  map monom2list (poly2list t);
wneuper@59523: 	val lls = sort_monList ll;
wneuper@59523: 	val T = type_of t;
wneuper@59523: 	val ls = map (create_monom T) lls;
wneuper@59523:     in create_polynom T ls end;
wneuper@59523: \<close>
wneuper@59523: 
wneuper@59523: subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>
wneuper@59523: ML \<open>
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
walther@59603:      "Prog_Expr.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)
wneuper@59523:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
wneuper@59523:   | dest_hd' t = raise TERM ("dest_hd'", [t]);
neuper@37950: 
neuper@37950: fun size_of_term' (Const(str,_) $ t) =
walther@59603:   if "Prog_Expr.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@52070:     (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@52070:     (if pr then 
neuper@52070: 	   let
neuper@52070:        val (f, ts) = strip_comb t and (g, us) = strip_comb u;
wneuper@59416:        val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^
wneuper@59416:          commas (map (Rule.term_to_string''' thy) ts) ^ "]\"");
wneuper@59416:        val _ = tracing("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^
wneuper@59416:          commas (map (Rule.term_to_string''' thy) us) ^ "]\"");
neuper@52070:        val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
neuper@52070:          string_of_int (size_of_term' u) ^ ")");
neuper@52070:        val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o hd_ord) (f,g));
neuper@52070:        val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
neuper@52070:        val _ = tracing ("-------");
neuper@52070:      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)
wneuper@59523: and terms_ord _ pr (ts, us) = 
wneuper@59592:     list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
neuper@52070: 
neuper@37950: in
neuper@37950: 
wneuper@59416: fun ord_make_polynomial (pr:bool) thy (_: Rule.subst) tu = 
neuper@37950:     (term_ord' pr thy(***) tu = LESS );
neuper@37950: 
neuper@37950: end;(*local*)
neuper@37950: 
wneuper@59523: Rule.rew_ord' := overwritel (! Rule.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
wneuper@59523: [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
wneuper@59523: \<close>
neuper@37950: 
wneuper@59523: subsection \<open>predicates\<close>
wneuper@59523: subsubsection \<open>in specifications\<close>
wneuper@59523: ML \<open>
wneuper@59523: (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
wneuper@59523: fun is_polyrat_in t v = 
wneuper@59524:   let
wneuper@59523:    	fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:")
wneuper@59523: 	    (* at the moment there is no term like this, but ....*)
walther@59603: 	  | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)
wneuper@59524: 	  | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
wneuper@59524: 	  | finddivide (_ $ t1) v = finddivide t1 v
wneuper@59523: 	  | finddivide _ _ = false;
wneuper@59524:   in finddivide t v end;
wneuper@59523:     
wneuper@59524: fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
wneuper@59524: fun is_poly_in t v =     case poly_deg_in t v of SOME _ => true | NONE => false;
wneuper@59524: fun has_degree_in t v =  case expand_deg_in t v of SOME d => d | NONE => ~1;
neuper@37950: 
wneuper@59523: (*.the expression contains + - * ^ only ?
wneuper@59523:    this is weaker than 'is_polynomial' !.*)
wneuper@59523: fun is_polyexp (Free _) = true
wneuper@59529:   | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)
wneuper@59523:   | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
wneuper@59523:   | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
wneuper@59523:   | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
walther@59603:   | is_polyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
wneuper@59523:   | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
wneuper@59523:                ((is_polyexp t1) andalso (is_polyexp t2))
wneuper@59523:   | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = 
wneuper@59523:                ((is_polyexp t1) andalso (is_polyexp t2))
wneuper@59523:   | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = 
wneuper@59523:                ((is_polyexp t1) andalso (is_polyexp t2))
walther@59603:   | is_polyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) = 
wneuper@59523:                ((is_polyexp t1) andalso (is_polyexp t2))
wneuper@59523:   | is_polyexp _ = false;
wneuper@59523: \<close>
neuper@37950: 
wneuper@59523: subsubsection \<open>for hard-coded AC rewriting\<close>
wneuper@59523: ML \<open>
wneuper@59523: (* auch Klammerung muss übereinstimmen;
wneuper@59523:    sort_variables klammert Produkte rechtslastig*)
wneuper@59523: fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
wneuper@59523: 
wneuper@59523: fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
wneuper@59523: \<close>
wneuper@59523: 
wneuper@59523: subsection \<open>evaluations functions\<close>
wneuper@59523: subsubsection \<open>for predicates\<close>
wneuper@59523: ML \<open>
wneuper@59523: fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _  =
wneuper@59523:     if is_polyrat_in t v 
wneuper@59523:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59523:     else SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
wneuper@59523:   | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
wneuper@59523: 
wneuper@59523: (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
wneuper@59523: fun eval_is_expanded_in _ _ 
wneuper@59523:        (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
wneuper@59523:     if is_expanded_in t v
wneuper@59523:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59523:     else SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
wneuper@59523:   | eval_is_expanded_in _ _ _ _ = NONE;
wneuper@59523: 
wneuper@59523: (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
wneuper@59523: fun eval_is_poly_in _ _ 
wneuper@59523:        (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
wneuper@59523:     if is_poly_in t v
wneuper@59523:     then SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
wneuper@59523:     else SOME ((Rule.term2str p) ^ " = True",
wneuper@59523: 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
wneuper@59523:   | eval_is_poly_in _ _ _ _ = NONE;
wneuper@59523: 
wneuper@59523: (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
wneuper@59523: fun eval_has_degree_in _ _ 
wneuper@59523: 	     (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
wneuper@59523:     let val d = has_degree_in t v
wneuper@59523: 	val d' = TermC.term_of_num HOLogic.realT d
wneuper@59523:     in SOME ((Rule.term2str p) ^ " = " ^ (string_of_int d),
wneuper@59523: 	      HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
wneuper@59523:     end
wneuper@59523:   | eval_has_degree_in _ _ _ _ = NONE;
wneuper@59523: 
wneuper@59523: (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
wneuper@59523: fun eval_is_polyexp (thmid:string) _ 
wneuper@59523: 		       (t as (Const("Poly.is'_polyexp", _) $ arg)) thy = 
wneuper@59523:     if is_polyexp arg
wneuper@59523:     then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59523:     else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
wneuper@59523:   | eval_is_polyexp _ _ _ _ = NONE; 
wneuper@59523: \<close>
wneuper@59523: 
wneuper@59523: subsubsection \<open>for hard-coded AC rewriting\<close>
wneuper@59523: ML \<open>
wneuper@59523: (*WN.18.6.03 *)
wneuper@59523: (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
wneuper@59523: fun eval_is_addUnordered (thmid:string) _ 
wneuper@59523: 		       (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy = 
wneuper@59523:     if is_addUnordered arg
wneuper@59523:     then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59523:     else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
wneuper@59523:   | eval_is_addUnordered _ _ _ _ = NONE; 
wneuper@59523: 
wneuper@59523: fun eval_is_multUnordered (thmid:string) _ 
wneuper@59523: 		       (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy = 
wneuper@59523:     if is_multUnordered arg
wneuper@59523:     then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59523:     else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 
wneuper@59523: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
wneuper@59523:   | eval_is_multUnordered _ _ _ _ = NONE; 
wneuper@59523: \<close>
wneuper@59526: setup \<open>KEStore_Elems.add_calcs
wneuper@59526:   [("is_polyrat_in", ("Poly.is'_polyrat'_in",
wneuper@59526: 		    eval_is_polyrat_in "#eval_is_polyrat_in")),
wneuper@59526:     ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
wneuper@59526:     ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
wneuper@59526:     ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
wneuper@59526:     ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
wneuper@59526:     ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
wneuper@59526:     ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))]\<close>
wneuper@59523: 
wneuper@59523: subsection \<open>rule-sets\<close>
wneuper@59523: subsubsection \<open>without specific order\<close>
wneuper@59523: ML \<open>
wneuper@59523: (* used only for merge *)
wneuper@59523: val calculate_Poly = Rule.append_rls "calculate_PolyFIXXXME.not.impl." Rule.e_rls [];
wneuper@59523: 
wneuper@59523: (*.for evaluation of conditions in rewrite rules.*)
wneuper@59523: val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls
walther@59603:   [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
wneuper@59523:   Rule.Thm  ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
walther@59603:   Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59603:   Rule.Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
walther@59603:   Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603:   Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")];
wneuper@59523: 
wneuper@59523: val poly_crls = Rule.append_rls "poly_crls" Atools_crls
walther@59603:   [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
wneuper@59523:   Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
walther@59603:   Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59603:   Rule.Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
walther@59603:   Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603:   Rule.Calc ("Prog_Expr.pow" , (**)eval_binop "#power_")];
wneuper@59523: \<close>
wneuper@59523: ML \<open>
neuper@37950: val expand =
wneuper@59416:   Rule.Rls {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	       Rule.Thm ("distrib_left", TermC.num_str @{thm distrib_left})
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37980: val discard_minus =
wneuper@59416:   Rule.Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
neuper@42407:       rules =
wneuper@59416:        [Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
neuper@42407:           (*"a - b = a + -1 * b"*)
wneuper@59416: 	        Rule.Thm ("sym_real_mult_minus1", TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@42407: 	          (*- ?z = "-1 * ?z"*)],
wneuper@59416: 	      scr = Rule.EmptyScr};
neuper@37980: 
neuper@37950: val expand_poly_ = 
wneuper@59416:   Rule.Rls{id = "expand_poly_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
neuper@42407:       rules =
wneuper@59416:         [Rule.Thm ("real_plus_binom_pow4", TermC.num_str @{thm real_plus_binom_pow4}),
neuper@42407: 	           (*"(a + b)^^^4 = ... "*)
wneuper@59416: 	         Rule.Thm ("real_plus_binom_pow5",TermC.num_str @{thm real_plus_binom_pow5}),
neuper@42407: 	           (*"(a + b)^^^5 = ... "*)
wneuper@59416: 	         Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
neuper@42407: 	           (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
neuper@42407: 	         (*WN071229 changed/removed for Schaerding -----vvv*)
wneuper@59416: 	         (*Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),*)
neuper@42407: 	           (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
wneuper@59416: 	         Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
neuper@42407: 	           (*"(a + b)^^^2 = (a + b) * (a + b)"*)
wneuper@59416: 	         (*Rule.Thm ("real_plus_minus_binom1_p_p", TermC.num_str @{thm real_plus_minus_binom1_p_p}),*)
neuper@42407: 	           (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
wneuper@59416: 	         (*Rule.Thm ("real_plus_minus_binom2_p_p", TermC.num_str @{thm real_plus_minus_binom2_p_p}),*)
neuper@42407: 	           (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@42407: 	         (*WN071229 changed/removed for Schaerding -----^^^*)
neuper@37950: 	      
wneuper@59416: 	         Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
neuper@42407: 	           (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	         Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
neuper@42407: 	           (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
wneuper@59416: 	         Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
neuper@42407: 	           (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
wneuper@59416: 	         Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
neuper@42407: 	           (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val expand_poly_rat_ = 
wneuper@59416:   Rule.Rls{id = "expand_poly_rat_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls =  Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
wneuper@59416: 	        [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")
neuper@37950: 		 ],
wneuper@59416:       srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
neuper@37950:       rules = 
wneuper@59416:         [Rule.Thm ("real_plus_binom_pow4_poly", TermC.num_str @{thm real_plus_binom_pow4_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
wneuper@59416: 	 Rule.Thm ("real_plus_binom_pow5_poly", TermC.num_str @{thm real_plus_binom_pow5_poly}),
neuper@37950: 	     (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
wneuper@59416: 	 Rule.Thm ("real_plus_binom_pow2_poly",TermC.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"*)
wneuper@59416: 	 Rule.Thm ("real_plus_binom_pow3_poly",TermC.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" *)
wneuper@59416: 	 Rule.Thm ("real_plus_minus_binom1_p_p",TermC.num_str @{thm real_plus_minus_binom1_p_p}),
neuper@37950: 	     (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
wneuper@59416: 	 Rule.Thm ("real_plus_minus_binom2_p_p",TermC.num_str @{thm real_plus_minus_binom2_p_p}),
neuper@37950: 	     (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 	      
wneuper@59416: 	 Rule.Thm ("real_add_mult_distrib_poly",
wneuper@59389:                TermC.num_str @{thm real_add_mult_distrib_poly}),
neuper@37950: 	       (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	 Rule.Thm("real_add_mult_distrib2_poly",
wneuper@59389:               TermC.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: 	       
wneuper@59416: 	 Rule.Thm ("realpow_multI_poly", TermC.num_str @{thm realpow_multI_poly}),
neuper@37950: 	     (*"[| r is_polyexp; s is_polyexp |] ==> 
neuper@37950: 		            (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
wneuper@59416: 	  Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
neuper@37950: 	      (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
wneuper@59416: 	 ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val simplify_power_ = 
wneuper@59416:   Rule.Rls{id = "simplify_power_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
neuper@37950: 		a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
wneuper@59416: 	       Rule.Thm ("sym_realpow_twoI",
wneuper@59389:                      TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),	
neuper@37950: 	       (*"r * r = r ^^^ 2"*)
wneuper@59416: 	       Rule.Thm ("realpow_twoI_assoc_l",TermC.num_str @{thm realpow_twoI_assoc_l}),
neuper@37950: 	       (*"r * (r * s) = r ^^^ 2 * s"*)
neuper@37950: 
wneuper@59416: 	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),		
neuper@37950: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
wneuper@59416: 	       Rule.Thm ("realpow_plus_1_assoc_l",
wneuper@59389:                      TermC.num_str @{thm realpow_plus_1_assoc_l}),
neuper@37950: 	       (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
wneuper@59416: 	       (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
wneuper@59416: 	       Rule.Thm ("realpow_plus_1_assoc_l2",
wneuper@59389:                      TermC.num_str @{thm realpow_plus_1_assoc_l2}),
neuper@37950: 	       (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
neuper@37950: 
wneuper@59416: 	       Rule.Thm ("sym_realpow_addI",
wneuper@59389:                TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950: 	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
wneuper@59416: 	       Rule.Thm ("realpow_addI_assoc_l",TermC.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*)
wneuper@59416: 	       Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
neuper@37950: 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val calc_add_mult_pow_ = 
wneuper@59416:   Rule.Rls{id = "calc_add_mult_pow_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
walther@59603:       calc = [("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_")), 
walther@59603: 	      ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 	      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
neuper@37950: 	      ],
neuper@42451:       errpatts = [],
walther@59603:       rules = [Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	       Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val reduce_012_mult_ = 
wneuper@59416:   Rule.Rls{id = "reduce_012_mult_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
wneuper@59416:                Rule.Thm ("mult_1_right",TermC.num_str @{thm mult_1_right}),
neuper@37950: 	       (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*) 
wneuper@59416: 	       Rule.Thm ("realpow_zeroI",TermC.num_str @{thm realpow_zeroI}),
neuper@37950: 	       (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
wneuper@59416: 	       Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
neuper@37950: 	       (*"r ^^^ 1 = r"*)
wneuper@59416: 	       Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
neuper@37950: 	       (*"1 ^^^ n = 1"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val collect_numerals_ = 
wneuper@59416:   Rule.Rls{id = "collect_numerals_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls, srls = Rule.Erls,
walther@59603:       calc = [("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
neuper@42451: 	      ], errpatts = [],
neuper@37950:       rules = 
wneuper@59416:         [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
neuper@37950: 	     (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
wneuper@59416: 	 Rule.Thm ("real_num_collect_assoc_r",TermC.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"*)
wneuper@59416: 	 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),	
neuper@37950: 	     (*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59416: 	 Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}), 
neuper@37950: 	     (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
neuper@37950: 
walther@59603:          Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
neuper@37950: 
wneuper@59416: 	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
neuper@37950: 		     (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
wneuper@59416:          Rule.Thm ("real_mult_2_assoc_r",TermC.num_str @{thm real_mult_2_assoc_r}),
neuper@37950: 	     (*"(k + z1) + z1 = k + 2 * z1"*)
wneuper@59416: 	 Rule.Thm ("sym_real_mult_2",TermC.num_str (@{thm real_mult_2} RS @{thm sym}))
neuper@37950: 	     (*"z1 + z1 = 2 * z1"*)
wneuper@59416: 	], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val reduce_012_ = 
wneuper@59416:   Rule.Rls{id = "reduce_012_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                 
neuper@37950: 	       (*"1 * z = z"*)
wneuper@59416: 	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),        
neuper@37950: 	       (*"0 * z = 0"*)
wneuper@59416: 	       Rule.Thm ("mult_zero_right",TermC.num_str @{thm mult_zero_right}),
neuper@37950: 	       (*"z * 0 = 0"*)
wneuper@59416: 	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
neuper@37950: 	       (*"0 + z = z"*)
wneuper@59416: 	       Rule.Thm ("add_0_right",TermC.num_str @{thm add_0_right}),
neuper@37950: 	       (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
neuper@37950: 
wneuper@59416: 	       (*Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI})*)
neuper@37950: 	       (*"?r ^^^ 1 = ?r"*)
wneuper@59416: 	       Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
neuper@37950: 	       (*"0 / ?x = 0"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37979: val discard_parentheses1 = 
wneuper@59416:     Rule.append_rls "discard_parentheses1" Rule.e_rls 
wneuper@59416: 	       [Rule.Thm ("sym_mult_assoc",
wneuper@59389:                       TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
neuper@37950: 		(*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
wneuper@59416: 		(*Rule.Thm ("sym_add_assoc",
wneuper@59389:                         TermC.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: 
wneuper@59523: val expand_poly =
wneuper@59416:   Rule.Rls{id = "expand_poly", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
neuper@37950:       (*asm_thm = [],*)
wneuper@59416:       rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	       Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
wneuper@59416: 	       (*Rule.Thm ("distrib_right1",TermC.num_str @{thm distrib_right}1),
neuper@37950: 		....... 18.3.03 undefined???*)
neuper@37950: 
wneuper@59416: 	       Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
neuper@37950: 	       (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
wneuper@59416: 	       Rule.Thm ("real_minus_binom_pow2_p",TermC.num_str @{thm real_minus_binom_pow2_p}),
neuper@37950: 	       (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
wneuper@59416: 	       Rule.Thm ("real_plus_minus_binom1_p",
wneuper@59389: 		    TermC.num_str @{thm real_plus_minus_binom1_p}),
neuper@37950: 	       (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
wneuper@59416: 	       Rule.Thm ("real_plus_minus_binom2_p",
wneuper@59389: 		    TermC.num_str @{thm real_plus_minus_binom2_p}),
neuper@37950: 	       (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 
wneuper@59416: 	       Rule.Thm ("minus_minus",TermC.num_str @{thm minus_minus}),
neuper@37950: 	       (*"- (- ?z) = ?z"*)
wneuper@59416: 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
neuper@37950: 	       (*"a - b = a + -1 * b"*)
wneuper@59416: 	       Rule.Thm ("sym_real_mult_minus1",
wneuper@59389:                      TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@37950: 	       (*- ?z = "-1 * ?z"*)
neuper@37950: 
wneuper@59416: 	       (*Rule.Thm ("real_minus_add_distrib",
wneuper@59389: 		      TermC.num_str @{thm real_minus_add_distrib}),*)
neuper@37950: 	       (*"- (?x + ?y) = - ?x + - ?y"*)
wneuper@59416: 	       (*Rule.Thm ("real_diff_plus",TermC.num_str @{thm real_diff_plus})*)
neuper@37950: 	       (*"a - b = a + -b"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
neuper@37950: val simplify_power = 
wneuper@59416:   Rule.Rls{id = "simplify_power", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
neuper@37950: 	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950: 	       
wneuper@59416: 	       Rule.Thm ("sym_realpow_twoI",
wneuper@59389:                      TermC.num_str( @{thm realpow_twoI} RS @{thm sym})),	
neuper@37950: 	       (*"r1 * r1 = r1 ^^^ 2"*)
wneuper@59416: 	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),		
neuper@37950: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
wneuper@59416: 	       Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
neuper@37950: 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
wneuper@59416: 	       Rule.Thm ("sym_realpow_addI",
wneuper@59389:                      TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950: 	       (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
wneuper@59416: 	       Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
neuper@37950: 	       (*"r ^^^ 1 = r"*)
wneuper@59416: 	       Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
neuper@37950: 	       (*"1 ^^^ n = 1"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@42451: 
neuper@37950: val collect_numerals = 
wneuper@59416:   Rule.Rls{id = "collect_numerals", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
walther@59603:       calc = [("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_")), 
walther@59603: 	      ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 	      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
neuper@42451: 	      ], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
neuper@37950: 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
wneuper@59416: 	       Rule.Thm ("real_num_collect_assoc",TermC.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"*)
wneuper@59416: 	       Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),	
neuper@37950: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59416: 	       Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
walther@59603: 	       Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	       Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: val reduce_012 = 
wneuper@59416:   Rule.Rls{id = "reduce_012", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                 
neuper@37950: 	       (*"1 * z = z"*)
wneuper@59416: 	       (*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),14.3.03*)
neuper@37950: 	       (*"-1 * z = - z"*)
wneuper@59416: 	       Rule.Thm ("minus_mult_left", 
wneuper@59389: 		    TermC.num_str (@{thm minus_mult_left} RS @{thm sym})),
neuper@37950: 	       (*- (?x * ?y) = "- ?x * ?y"*)
wneuper@59416: 	       (*Rule.Thm ("real_minus_mult_cancel",
wneuper@59389:                        TermC.num_str @{thm real_minus_mult_cancel}),
neuper@37950: 	       (*"- ?x * - ?y = ?x * ?y"*)---*)
wneuper@59416: 	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),        
neuper@37950: 	       (*"0 * z = 0"*)
wneuper@59416: 	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
neuper@37950: 	       (*"0 + z = z"*)
wneuper@59416: 	       Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),
neuper@37950: 	       (*"?z + - ?z = 0"*)
wneuper@59416: 	       Rule.Thm ("sym_real_mult_2",
wneuper@59389:                      TermC.num_str (@{thm real_mult_2} RS @{thm sym})),	
neuper@37950: 	       (*"z1 + z1 = 2 * z1"*)
wneuper@59416: 	       Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
neuper@37950: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@52139: 
neuper@37950: val discard_parentheses = 
wneuper@59416:     Rule.append_rls "discard_parentheses" Rule.e_rls 
wneuper@59416: 	       [Rule.Thm ("sym_mult_assoc",
wneuper@59389:                       TermC.num_str (@{thm mult.assoc} RS @{thm sym})),
wneuper@59416: 		Rule.Thm ("sym_add_assoc",
wneuper@59389:                       TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
wneuper@59523: \<close>
neuper@37950: 
wneuper@59523: subsubsection \<open>hard-coded AC rewriting\<close>
wneuper@59523: ML \<open>
wneuper@59523: (*MG.0401: termorders for multivariate polys dropped due to principal problems:
wneuper@59523:   (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
wneuper@59523: val order_add_mult = 
wneuper@59523:   Rule.Rls{id = "order_add_mult", preconds = [], 
wneuper@59523:       rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
wneuper@59523:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59523:       rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
wneuper@59523: 	       (* z * w = w * z *)
wneuper@59523: 	       Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
wneuper@59523: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
wneuper@59523: 	       Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),		
wneuper@59523: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
wneuper@59523: 	       Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),	
wneuper@59523: 	       (*z + w = w + z*)
wneuper@59416: 	       Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
wneuper@59523: 	       (*x + (y + z) = y + (x + z)*)
wneuper@59523: 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})	               
wneuper@59523: 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
wneuper@59523: 	       ], scr = Rule.EmptyScr};
wneuper@59523: (*MG.0401: termorders for multivariate polys dropped due to principal problems:
wneuper@59523:   (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
wneuper@59523: val order_mult = 
wneuper@59523:   Rule.Rls{id = "order_mult", preconds = [], 
wneuper@59523:       rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
wneuper@59523:       erls = Rule.e_rls,srls = Rule.Erls,
wneuper@59523:       calc = [], errpatts = [],
wneuper@59523:       rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
wneuper@59523: 	       (* z * w = w * z *)
wneuper@59523: 	       Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
wneuper@59523: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
wneuper@59523: 	       Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc})	
wneuper@59523: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
wneuper@59523: 	       ], scr = Rule.EmptyScr};
wneuper@59472: \<close>
wneuper@59472: ML \<open>
wneuper@59416: fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
wneuper@59416:     []:(Rule.rule * (term * term list)) list;
wneuper@59416: fun init_state (_: term) = Rule.e_rrlsstate;
wneuper@59416: fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
wneuper@59416:     ([]:(Rule.rule * (term * term list)) list);
wneuper@59416: fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
wneuper@59406: fun normal_form t = SOME (sort_variables t, []: term list);
neuper@37950: 
neuper@37950: val order_mult_ =
wneuper@59416:     Rule.Rrls {id = "order_mult_", 
neuper@37950: 	  prepat = 
neuper@38036:           (* ?p matched with the current term gives an environment,
neuper@38037:              which evaluates (the instantiated) "?p is_multUnordered" to true *)
wneuper@59389: 	  [([TermC.parse_patt thy "?p is_multUnordered"], 
wneuper@59389:              TermC.parse_patt thy "?p :: real")],
wneuper@59416: 	  rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416: 	  erls = Rule.append_rls "Rule.e_rls-is_multUnordered" Rule.e_rls
wneuper@59416: 			    [Rule.Calc ("Poly.is'_multUnordered", 
neuper@37976:                                     eval_is_multUnordered "")],
walther@59603: 	  calc = [("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
walther@59603: 		  ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 		  ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
walther@59603: 		  ("POWER" , ("Prog_Expr.pow", (**)eval_binop "#power_"))],
wneuper@59406:     errpatts = [],
wneuper@59416: 	  scr = Rule.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_ = 
wneuper@59416:   Rule.Rls {id = "order_mult_rls_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Rls_ order_mult_
wneuper@59416: 	       ], scr = Rule.EmptyScr};
neuper@37950: 
wneuper@59523: \<close> ML \<open>
neuper@37950: 
wneuper@59416: fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
wneuper@59416:     []: (Rule.rule * (term * term list)) list;
wneuper@59416: fun init_state (_: term) = Rule.e_rrlsstate;
wneuper@59416: fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
wneuper@59416:     ([]: (Rule.rule * (term * term list)) list);
wneuper@59416: fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
wneuper@59406: fun normal_form t = SOME (sort_monoms t,[]: term list);
wneuper@59472: \<close> ML \<open>
neuper@37950: val order_add_ =
wneuper@59416:     Rule.Rrls {id = "order_add_", 
neuper@37950: 	  prepat = (*WN.18.6.03 Preconditions und Pattern,
wneuper@59416: 		    die beide passen muessen, damit das Rule.Rrls angewandt wird*)
wneuper@59389: 	  [([TermC.parse_patt @{theory} "?p is_addUnordered"], 
wneuper@59389: 	     TermC.parse_patt @{theory} "?p :: real" 
neuper@37950: 	    (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment 
neuper@37950: 	      fuer die Evaluation der Precondition "p is_addUnordered"*))],
wneuper@59416: 	  rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416: 	  erls = Rule.append_rls "Rule.e_rls-is_addUnordered" Rule.e_rls(*MG: poly_erls*)
walther@59603: 			    [Rule.Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")],
walther@59603: 	  calc = [("PLUS"  ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
walther@59603: 		  ("TIMES" ,("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 		  ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
walther@59603: 		  ("POWER" ,("Prog_Expr.pow"  , (**)eval_binop "#power_"))],
neuper@42451: 	  errpatts = [],
wneuper@59416: 	  scr = Rule.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: 
wneuper@59406: val order_add_rls_ =
wneuper@59416:   Rule.Rls {id = "order_add_rls_", preconds = [], 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Rule.e_rls,srls = Rule.Erls,
neuper@42451:       calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Rls_ order_add_
wneuper@59416: 	       ], scr = Rule.EmptyScr};
wneuper@59472: \<close>
neuper@37950: 
wneuper@59472: text \<open>rule-set make_polynomial also named norm_Poly:
neuper@42398:   Rewrite order has not been implemented properly; the order is better in 
neuper@42398:   make_polynomial_in (coded in SML).
neuper@42398:   Notes on state of development:
neuper@42398:   \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
neuper@42398:   \# migration Isabelle2002 --> 2011 weakened the rule set, see test
neuper@42398:   --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37950: (*. see MG-DA.p.52ff .*)
neuper@37950: val make_polynomial(*MG.03, overwrites version from above, 
neuper@37950:     previously 'make_polynomial_'*) =
wneuper@59416:   Rule.Seq {id = "make_polynomial", preconds = []:term list, 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls, srls = Rule.Erls,calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Rls_ discard_minus,
wneuper@59416: 	       Rule.Rls_ expand_poly_,
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
wneuper@59416: 	       Rule.Rls_ order_mult_rls_,
wneuper@59416: 	       Rule.Rls_ simplify_power_, 
wneuper@59416: 	       Rule.Rls_ calc_add_mult_pow_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_mult_,
wneuper@59416: 	       Rule.Rls_ order_add_rls_,
wneuper@59416: 	       Rule.Rls_ collect_numerals_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_,
wneuper@59416: 	       Rule.Rls_ discard_parentheses1
neuper@37950: 	       ],
wneuper@59416:       scr = Rule.EmptyScr
wneuper@59406:       };
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37950: val norm_Poly(*=make_polynomial*) = 
wneuper@59416:   Rule.Seq {id = "norm_Poly", preconds = []:term list, 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Rls_ discard_minus,
wneuper@59416: 	       Rule.Rls_ expand_poly_,
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
wneuper@59416: 	       Rule.Rls_ order_mult_rls_,
wneuper@59416: 	       Rule.Rls_ simplify_power_, 
wneuper@59416: 	       Rule.Rls_ calc_add_mult_pow_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_mult_,
wneuper@59416: 	       Rule.Rls_ order_add_rls_,
wneuper@59416: 	       Rule.Rls_ collect_numerals_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_,
wneuper@59416: 	       Rule.Rls_ discard_parentheses1
neuper@37950: 	       ],
wneuper@59416:       scr = Rule.EmptyScr
wneuper@59406:       };
wneuper@59472: \<close>
wneuper@59472: ML \<open>
wneuper@59416: (* MG:03 Like make_polynomial_ but without Rule.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 =
wneuper@59416:   Rule.Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list, 
wneuper@59416:       rew_ord = ("dummy_ord", Rule.dummy_ord),
wneuper@59416:       erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Rls_ discard_minus,
wneuper@59416: 	       Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
wneuper@59416: 	       Rule.Rls_ order_mult_rls_,
wneuper@59416: 	       Rule.Rls_ simplify_power_, 
wneuper@59416: 	       Rule.Rls_ calc_add_mult_pow_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_mult_,
wneuper@59416: 	       Rule.Rls_ order_add_rls_,
wneuper@59416: 	       Rule.Rls_ collect_numerals_, 
wneuper@59416: 	       Rule.Rls_ reduce_012_
wneuper@59416: 	       (*Rule.Rls_ discard_parentheses1 *)
neuper@37950: 	       ],
wneuper@59416:       scr = Rule.EmptyScr
wneuper@59406:       };
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37950: (*.a minimal ruleset for reverse rewriting of factions [2];
neuper@37950:    compare expand_binoms.*)
neuper@37950: val rev_rew_p = 
wneuper@59416: Rule.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
wneuper@59416:     erls = Atools_erls, srls = Rule.Erls,
walther@59603:     calc = [(*("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_")), 
walther@59603: 	    ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 	    ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))*)
neuper@42451: 	    ], errpatts = [],
wneuper@59416:     rules = [Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
neuper@37950: 	     (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
wneuper@59416: 	     Rule.Thm ("real_plus_binom_times1" ,TermC.num_str @{thm real_plus_binom_times1}),
neuper@37950: 	     (*"(a +  1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
wneuper@59416: 	     Rule.Thm ("real_plus_binom_times2" ,TermC.num_str @{thm real_plus_binom_times2}),
neuper@37950: 	     (*"(a + -1*b)*(a +  1*b) = a^^^2 + -1*b^^^2"*)
neuper@37950: 
wneuper@59416: 	     Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
neuper@37950: 
wneuper@59416:              Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
neuper@37950: 	     (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	     Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
neuper@37950: 	     (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
wneuper@59416: 	     Rule.Thm ("mult_assoc", TermC.num_str @{thm mult.assoc}),
neuper@37950: 	     (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
wneuper@59416: 	     Rule.Rls_ order_mult_rls_,
wneuper@59416: 	     (*Rule.Rls_ order_add_rls_,*)
neuper@37950: 
walther@59603: 	     Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59603: 	     Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	     Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
neuper@37950: 	     
wneuper@59416: 	     Rule.Thm ("sym_realpow_twoI",
wneuper@59389:                    TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950: 	     (*"r1 * r1 = r1 ^^^ 2"*)
wneuper@59416: 	     Rule.Thm ("sym_real_mult_2",
wneuper@59389:                    TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950: 	     (*"z1 + z1 = 2 * z1"*)
wneuper@59416: 	     Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
neuper@37950: 	     (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37950: 
wneuper@59416: 	     Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
neuper@37950: 	     (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
wneuper@59416: 	     Rule.Thm ("real_num_collect_assoc",TermC.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"*)
wneuper@59416: 	     Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
neuper@37950: 	     (*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59416: 	     Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 
neuper@37950: 	     (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37950: 
wneuper@59416: 	     Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
neuper@37950: 	     (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950: 
walther@59603: 	     Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59603: 	     Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	     Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
neuper@37950: 
wneuper@59416: 	     Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
wneuper@59416: 	     Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
wneuper@59416: 	     Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left})(*0 + z = z*)
neuper@37950: 
wneuper@59416: 	     (*Rule.Rls_ order_add_rls_*)
neuper@37950: 	     ],
neuper@37950: 
wneuper@59416:     scr = Rule.EmptyScr};      
wneuper@59472: \<close>
neuper@52125: 
wneuper@59523: subsection \<open>rule-sets with explicit program for intermediate steps\<close>
wneuper@59523: partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
wneuper@59523:   where
wneuper@59552: "expand_binoms_2 term =
wneuper@59523: (Repeat                                                           
wneuper@59523: ((Try (Repeat (Rewrite ''real_plus_binom_pow2''    False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_plus_binom_times''   False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_minus_binom_pow2''   False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_minus_binom_times''  False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_plus_minus_binom1''  False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_plus_minus_binom2''  False))) @@    
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Rewrite ''mult_1_left''             False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''mult_zero_left''             False))) @@ 
wneuper@59523:  (Try (Repeat (Rewrite ''add_0_left''      False))) @@            
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Calculate ''PLUS''  ))) @@                         
wneuper@59523:  (Try (Repeat (Calculate ''TIMES'' ))) @@                         
wneuper@59523:  (Try (Repeat (Calculate ''POWER''))) @@                          
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Rewrite ''sym_realpow_twoI''        False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''realpow_plus_1''          False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''sym_real_mult_2''         False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_mult_2_assoc''       False))) @@    
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Rewrite ''real_num_collect''        False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_num_collect_assoc''  False))) @@    
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Rewrite ''real_one_collect''        False))) @@    
wneuper@59523:  (Try (Repeat (Rewrite ''real_one_collect_assoc''  False))) @@    
wneuper@59523:                                                                   
wneuper@59523:  (Try (Repeat (Calculate ''PLUS''  ))) @@                         
wneuper@59523:  (Try (Repeat (Calculate ''TIMES'' ))) @@                         
wneuper@59523:  (Try (Repeat (Calculate ''POWER''))))                            
wneuper@59523:  term)                                                             "
wneuper@59523: ML \<open>
wneuper@59523: val expand_binoms = 
wneuper@59523:   Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
wneuper@59523:       erls = Atools_erls, srls = Rule.Erls,
walther@59603:       calc = [("PLUS"  , ("Groups.plus_class.plus", (**)eval_binop "#add_")), 
walther@59603: 	      ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603: 	      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
wneuper@59523: 	      ], errpatts = [],
wneuper@59523:       rules = [Rule.Thm ("real_plus_binom_pow2",
wneuper@59523:                      TermC.num_str @{thm real_plus_binom_pow2}),     
wneuper@59523: 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
wneuper@59523: 	       Rule.Thm ("real_plus_binom_times",
wneuper@59523:                      TermC.num_str @{thm real_plus_binom_times}),    
wneuper@59523: 	      (*"(a + b)*(a + b) = ...*)
wneuper@59523: 	       Rule.Thm ("real_minus_binom_pow2",
wneuper@59523:                      TermC.num_str @{thm real_minus_binom_pow2}),   
wneuper@59523: 	       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
wneuper@59523: 	       Rule.Thm ("real_minus_binom_times",
wneuper@59523:                      TermC.num_str @{thm real_minus_binom_times}),   
wneuper@59523: 	       (*"(a - b)*(a - b) = ...*)
wneuper@59523: 	       Rule.Thm ("real_plus_minus_binom1",
wneuper@59523:                      TermC.num_str @{thm real_plus_minus_binom1}),   
wneuper@59523: 		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
wneuper@59523: 	       Rule.Thm ("real_plus_minus_binom2",
wneuper@59523:                      TermC.num_str @{thm real_plus_minus_binom2}),   
wneuper@59523: 		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
wneuper@59523: 	       (*RL 020915*)
wneuper@59523: 	       Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), 
wneuper@59523: 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
wneuper@59523:                Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), 
wneuper@59523: 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
wneuper@59523:                Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), 
wneuper@59523: 		(*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
wneuper@59523:                Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), 
wneuper@59523: 		(*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
wneuper@59523: 	       Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
wneuper@59523: 		(*(a*b)^^^n = a^^^n * b^^^n*)
wneuper@59523: 	       Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
wneuper@59523: 	        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
wneuper@59523: 	       Rule.Thm ("real_minus_binom_pow3",
wneuper@59523:                      TermC.num_str @{thm real_minus_binom_pow3}),
wneuper@59523: 	        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
wneuper@59523: 
wneuper@59523: 
wneuper@59523:               (*Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),	
wneuper@59523: 		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59523: 	       Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),	
wneuper@59523: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
wneuper@59523: 	       Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),	
wneuper@59523: 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
wneuper@59523: 	       Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),	
wneuper@59523: 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
wneuper@59523: 	      *)
wneuper@59523: 	       Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
wneuper@59523:                (*"1 * z = z"*)
wneuper@59523: 	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
wneuper@59523:                (*"0 * z = 0"*)
wneuper@59523: 	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),(*"0 + z = z"*)
wneuper@59523: 
walther@59603: 	       Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	       Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
wneuper@59523:               (*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
wneuper@59523: 		(*AC-rewriting*)
wneuper@59523: 	       Rule.Thm ("real_mult_left_commute",
wneuper@59523:                      TermC.num_str @{thm real_mult_left_commute}),
wneuper@59523: 	       Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
wneuper@59523: 	       Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
wneuper@59523: 	       Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
wneuper@59523: 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
wneuper@59523: 	      *)
wneuper@59523: 	       Rule.Thm ("sym_realpow_twoI",
wneuper@59523:                      TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
wneuper@59523: 	       (*"r1 * r1 = r1 ^^^ 2"*)
wneuper@59523: 	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),			
wneuper@59523: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
wneuper@59523: 	       (*Rule.Thm ("sym_real_mult_2",
wneuper@59523:                        TermC.num_str (@{thm real_mult_2} RS @{thm sym})),		
wneuper@59523: 	       (*"z1 + z1 = 2 * z1"*)*)
wneuper@59523: 	       Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),		
wneuper@59523: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
wneuper@59523: 
wneuper@59523: 	       Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
wneuper@59523: 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
wneuper@59523: 	       Rule.Thm ("real_num_collect_assoc",
wneuper@59523:                      TermC.num_str @{thm real_num_collect_assoc}),	
wneuper@59523: 	       (*"[| l is_const; m is_const |] ==>  
wneuper@59523:                                        l * n + (m * n + k) =  (l + m) * n + k"*)
wneuper@59523: 	       Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
wneuper@59523: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59523: 	       Rule.Thm ("real_one_collect_assoc",
wneuper@59523:                      TermC.num_str @{thm real_one_collect_assoc}), 
wneuper@59523: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
wneuper@59523: 
walther@59603: 	       Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59603: 	       Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59603: 	       Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
wneuper@59523: 	       ],
wneuper@59552:       scr = Rule.Prog (LTool.prep_program @{thm expand_binoms_2.simps})
wneuper@59523:       };      
wneuper@59523: \<close>
wneuper@59523: 
wneuper@59523: subsection \<open>add to KEStore\<close>
wneuper@59523: subsubsection \<open>rule-sets\<close>
wneuper@59472: ML \<open>val prep_rls' = LTool.prep_rls @{theory}\<close>
s1210629013@55444: 
wneuper@59472: setup \<open>KEStore_Elems.add_rlss 
s1210629013@55444:   [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)), 
s1210629013@55444:   ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*) 
s1210629013@55444:   ("expand", (Context.theory_name @{theory}, prep_rls' expand)), 
s1210629013@55444:   ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)), 
s1210629013@55444:   ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
neuper@52125: 
s1210629013@55444:   ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)), 
s1210629013@55444:   ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)), 
s1210629013@55444:   ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)), 
s1210629013@55444:   ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)), 
s1210629013@55444:   ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
neuper@52125:  
s1210629013@55444:   ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)), 
s1210629013@55444:   ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)), 
s1210629013@55444:   ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)), 
s1210629013@55444:   ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)), 
s1210629013@55444:   ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
neuper@52125:  
s1210629013@55444:   ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)), 
s1210629013@55444:   ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)), 
s1210629013@55444:   ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)), 
s1210629013@55444:   ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)), 
s1210629013@55444:   ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
neuper@52125:  
s1210629013@55444:   ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)), 
s1210629013@55444:   ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)), 
s1210629013@55444:   ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)), 
neuper@52125:   ("make_rat_poly_with_parentheses",
wneuper@59472:     (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close>
wneuper@59523: 
wneuper@59526: subsection \<open>problems\<close>
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
wneuper@59406:   [(Specify.prep_pbt thy "pbl_simp_poly" [] Celem.e_pblID
s1210629013@55339:       (["polynomial","simplification"],
s1210629013@55339:         [("#Given" ,["Term t_t"]),
s1210629013@55339:           ("#Where" ,["t_t is_polyexp"]),
s1210629013@55339:           ("#Find"  ,["normalform n_n"])],
wneuper@59416:         Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)
wneuper@59416: 			  Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
s1210629013@55339:         SOME "Simplify t_t", 
wneuper@59472:         [["simplification","for_polynomials"]]))]\<close>
wneuper@59429: 
wneuper@59526: subsection \<open>methods\<close>
wneuper@59545: 
wneuper@59429: partial_function (tailrec) simplify :: "real \<Rightarrow> real"
wneuper@59429:   where
wneuper@59504: "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
s1210629013@55373: 	    (["simplification","for_polynomials"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]),
s1210629013@55373: 	        ("#Where" ,["t_t is_polyexp"]),
s1210629013@55373: 	        ("#Find"  ,["normalform n_n"])],
wneuper@59416: 	      {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, 
wneuper@59416: 	        prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls 
s1210629013@55373: 				    [(*for preds in where_*)
walther@59603: 				      Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp"")],
wneuper@59416: 				  crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
wneuper@59552:         @{thm simplify.simps})]
wneuper@59472: \<close>
wneuper@59472: ML \<open>
wneuper@59472: \<close> ML \<open>
wneuper@59472: \<close> 
neuper@37906: end