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" wneuper@59334: ("((Script Expand'_binoms (_ =))// (_))" 9) neuper@37906: neuper@37906: (*-------------------- rules------------------------------------------------*) 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 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: 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: 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 = wneuper@59389: let fun coeff_in c v = member op = (TermC.vars c) v; neuper@38031: fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:") neuper@37950: (* at the moment there is no term like this, but ....*) wneuper@59360: | finddivide (t as (Const ("Rings.divide_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 wneuper@59416: then SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) wneuper@59416: else SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) 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.*) wneuper@59389: fun coeff_in c v = not (member op = (TermC.vars c) v); neuper@37950: (* FIXME.WN100826 shift this into test-------------- wneuper@59186: val v = (Thm.term_of o the o (parse thy)) "x"; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "1"; neuper@37950: coeff_in t v; neuper@37950: (*val it = true : bool*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "a*b+c"; neuper@37950: coeff_in t v; neuper@37950: (*val it = true : bool*) wneuper@59186: val t = (Thm.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@38034: (t as Const ("Groups.times_class.times",_) $ t1 $ neuper@37950: (Const ("Atools.pow",_) $ vv $ Free (d,_))) v = wneuper@59390: if ((vv = v) andalso (coeff_in t1 v)) then SOME (TermC.int_of_str d) else NONE neuper@37950: | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v = wneuper@59390: if (vv = v) then SOME (TermC.int_of_str d) else NONE neuper@38034: | factor_right_deg (t as Const ("Groups.times_class.times",_) $ 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----------------------------- wneuper@59186: val v = (Thm.term_of o the o (parse thy)) "x"; wneuper@59186: val t = (Thm.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*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "x^^^7"; neuper@37950: mono_deg_in t v; neuper@37950: (*val it = SOME 7*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x"; neuper@37950: mono_deg_in t v; neuper@37950: (*val it = SOME 1*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x"; neuper@37950: mono_deg_in t v; neuper@37950: (*val it = NONE*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "x"; neuper@37950: mono_deg_in t v; neuper@37950: (*val it = SOME 1*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "(a*b+c)"; neuper@37950: mono_deg_in t v; neuper@37950: (*val it = SOME 0*) wneuper@59186: val t = (Thm.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----------------------------- wneuper@59186: val v = (Thm.term_of o the o (parse thy)) "x"; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "a+b"; neuper@37950: expand_deg_in t v; neuper@37950: (*val it = SOME 0*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "(a+b)*x"; neuper@37950: expand_deg_in t v; neuper@37950: (*SOME 1*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x"; neuper@37950: expand_deg_in t v; neuper@37950: (*SOME 1*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "a*b + (a-b)*x"; neuper@37950: expand_deg_in t v; neuper@37950: (*SOME 1*) wneuper@59186: val t = (Thm.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----------------------------- wneuper@59186: val v = (Thm.term_of o the o (parse thy)) "x"; wneuper@59186: val t = (Thm.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*) wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "-8 - 2*x + x^^^2"; neuper@37950: has_degree_in t v; neuper@37950: (*val it = 2*) wneuper@59186: val t = (Thm.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 wneuper@59416: then SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) wneuper@59416: else SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) neuper@37950: | eval_is_expanded_in _ _ _ _ = NONE; neuper@37950: (* wneuper@59186: val t = (Thm.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"*) wneuper@59416: Rule.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 wneuper@59416: then SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) wneuper@59416: else SOME ((Rule.term2str p) ^ " = True", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) neuper@37950: | eval_is_poly_in _ _ _ _ = NONE; neuper@37950: (* wneuper@59186: val t = (Thm.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"*) wneuper@59416: Rule.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 wneuper@59389: val d' = TermC.term_of_num HOLogic.realT d wneuper@59416: in SOME ((Rule.term2str p) ^ " = " ^ (string_of_int d), wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (p, d'))) neuper@37950: end neuper@37950: | eval_has_degree_in _ _ _ _ = NONE; neuper@37950: (* wneuper@59186: > val t = (Thm.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 wneuper@59416: > Rule.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 = wneuper@59416: Rule.append_rls "calculate_PolyFIXXXME.not.impl." Rule.e_rls neuper@37978: []; neuper@37978: neuper@37950: (*.for evaluation of conditions in rewrite rules.*) wneuper@59416: val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls wneuper@59416: [Rule.Calc ("HOL.eq", eval_equal "#equal_"), wneuper@59416: Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_")]; neuper@37950: wneuper@59416: val poly_crls = Rule.append_rls "poly_crls" Atools_crls wneuper@59416: [Rule.Calc ("HOL.eq", eval_equal "#equal_"), wneuper@59416: Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow" ,eval_binop "#power_")]; 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*) wneuper@59390: (case TermC.int_of_str_opt (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@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) neuper@37950: and terms_ord str pr (ts, us) = wneuper@59406: list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(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: neuper@37950: wneuper@59416: Rule.rew_ord' := overwritel (! Rule.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 = 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@37950: (*----------------- Begin: rulesets for make_polynomial_ ----------------- neuper@37950: 'rlsIDs' redefined by MG as 'rlsIDs_' neuper@37950: ^^^*) 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: (*.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@38034: | is_polyexp (Const ("Groups.times_class.times",_) $ 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@38034: | is_polyexp (Const ("Groups.times_class.times",_) $ 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 wneuper@59416: then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) wneuper@59416: else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) neuper@37950: | eval_is_polyexp _ _ _ _ = NONE; 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, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37950: ("POWER", ("Atools.pow", eval_binop "#power_")) neuper@37950: ], neuper@42451: errpatts = [], wneuper@59416: rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.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, neuper@38014: 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: wneuper@59416: 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: 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 = 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, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37950: ("POWER", ("Atools.pow", eval_binop "#power_")) neuper@37950: ], 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 ==> n + (m * n + k) = (1 + m) * n + k"*) neuper@37950: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), neuper@37950: neuper@37950: (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*) 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@37950: 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@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@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 = wneuper@59416: Rule.Rls{id = "order_add_mult", preconds = [], neuper@37972: rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy), wneuper@59416: erls = Rule.e_rls,srls = Rule.Erls, neuper@42451: calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}), neuper@37950: (* z * w = w * z *) wneuper@59416: Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), neuper@37950: (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) wneuper@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), neuper@37950: (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) wneuper@59416: Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}), neuper@37950: (*z + w = w + z*) wneuper@59416: Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}), neuper@37950: (*x + (y + z) = y + (x + z)*) wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}) neuper@37950: (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) wneuper@59416: ], scr = Rule.EmptyScr}; 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 = wneuper@59416: Rule.Rls{id = "order_mult", preconds = [], neuper@37972: rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy), wneuper@59416: erls = Rule.e_rls,srls = Rule.Erls, neuper@42451: calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}), neuper@37950: (* z * w = w * z *) wneuper@59416: Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), neuper@37950: (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) wneuper@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}) neuper@37950: (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) wneuper@59416: ], scr = Rule.EmptyScr}; neuper@42451: *} neuper@42451: neuper@42451: ML {* 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, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37950: ("POWER", ("Atools.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"*) wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.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}))]; neuper@37950: wneuper@59429: (* probably perfectly replaced by auto-generated version *) 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@52062: " (Try (Repeat (Rewrite distrib_right False))) @@ " ^ neuper@52062: " (Try (Repeat (Rewrite distrib_left 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@48763: " (Try (Repeat (Rewrite mult_commute False))) @@ " ^ neuper@37950: " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^ neuper@48763: " (Try (Repeat (Rewrite 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 s1210629013@55444: val make_polynomial = prep_rls'( 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, neuper@42451: calc = [], errpatts = [], wneuper@59416: rules = [Rule.Rls_ expand_poly, wneuper@59416: Rule.Rls_ order_add_mult, wneuper@59416: Rule.Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *) wneuper@59416: Rule.Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *) wneuper@59416: Rule.Rls_ reduce_012, wneuper@59416: Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),(*in --^*) wneuper@59416: Rule.Rls_ discard_parentheses neuper@37950: ], wneuper@59416: scr = Rule.EmptyScr wneuper@59406: }); *) neuper@37950: wneuper@59429: (* replacement by auto-generated version seemed to cause ERROR in algein.sml *) 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 = wneuper@59416: Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), wneuper@59416: erls = Atools_erls, srls = Rule.Erls, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37950: ("POWER", ("Atools.pow", eval_binop "#power_")) neuper@42451: ], errpatts = [], wneuper@59416: rules = [Rule.Thm ("real_plus_binom_pow2", wneuper@59389: 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_plus_binom_times", wneuper@59389: TermC.num_str @{thm real_plus_binom_times}), neuper@37950: (*"(a + b)*(a + b) = ...*) wneuper@59416: Rule.Thm ("real_minus_binom_pow2", wneuper@59389: TermC.num_str @{thm real_minus_binom_pow2}), neuper@37950: (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) wneuper@59416: Rule.Thm ("real_minus_binom_times", wneuper@59389: TermC.num_str @{thm real_minus_binom_times}), neuper@37950: (*"(a - b)*(a - b) = ...*) wneuper@59416: Rule.Thm ("real_plus_minus_binom1", wneuper@59389: TermC.num_str @{thm real_plus_minus_binom1}), neuper@37950: (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) wneuper@59416: Rule.Thm ("real_plus_minus_binom2", wneuper@59389: TermC.num_str @{thm real_plus_minus_binom2}), neuper@37950: (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) neuper@37950: (*RL 020915*) wneuper@59416: Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), neuper@37950: (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) wneuper@59416: Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), neuper@37950: (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) wneuper@59416: Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), neuper@37950: (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*) wneuper@59416: Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), neuper@37950: (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*) wneuper@59416: Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}), neuper@37950: (*(a*b)^^^n = a^^^n * b^^^n*) wneuper@59416: Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}), neuper@37950: (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) wneuper@59416: Rule.Thm ("real_minus_binom_pow3", wneuper@59389: TermC.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: 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"*) wneuper@59416: Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}), neuper@37950: (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) wneuper@59416: Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}), neuper@37950: (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) neuper@37974: *) wneuper@59416: Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}), neuper@37974: (*"1 * z = z"*) wneuper@59416: Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}), neuper@37974: (*"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.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_"), wneuper@59416: (*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}), neuper@37974: (*AC-rewriting*) wneuper@59416: Rule.Thm ("real_mult_left_commute", wneuper@59389: TermC.num_str @{thm real_mult_left_commute}), wneuper@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), wneuper@59416: Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}), wneuper@59416: Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}), wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}), neuper@37974: *) 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 ("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@37974: (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*) wneuper@59416: Rule.Thm ("real_num_collect_assoc", wneuper@59389: TermC.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"*) 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", wneuper@59389: 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.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_") neuper@37950: ], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) scr_expand_binoms) wneuper@59406: }; 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@38034: fun monom2list (Const ("Groups.times_class.times",_) $ 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 = wneuper@59416: error("get_basStr: called with t= "^(Rule.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 = wneuper@59416: error("get_potStr: called with t= "^(Rule.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 wneuper@59389: | filter_num [Free x] = if (TermC.is_num (Free x)) then true neuper@37950: else false neuper@37950: | filter_num ((Free _)::_) = false neuper@37950: | filter_num ts = wneuper@59389: (filter_num o (filter_out TermC.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 wneuper@59390: counter (n + (the (TermC.int_of_str_opt 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) wneuper@59416: (*| _ => error("monom_degree: called with factor: "^(Rule.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@38034: fun mult T = Const ("Groups.times_class.times", [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@42451: *} neuper@42451: ML {* neuper@37950: fun eval_is_multUnordered (thmid:string) _ neuper@37950: (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy = neuper@37950: if is_multUnordered arg wneuper@59416: then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) wneuper@59416: else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) neuper@37950: | eval_is_multUnordered _ _ _ _ = NONE; 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_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 "")], neuper@38036: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38036: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), wneuper@59360: ("DIVIDE", ("Rings.divide_class.divide", neuper@38036: eval_cancel "#divide_e")), neuper@37976: ("POWER" , ("Atools.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@42451: *} neuper@42451: ML {* 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 wneuper@59416: then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) wneuper@59416: else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) neuper@37950: | eval_is_addUnordered _ _ _ _ = NONE; 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); neuper@37950: wneuper@59406: *} ML {* 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*) wneuper@59416: [Rule.Calc ("Poly.is'_addUnordered", neuper@38037: eval_is_addUnordered "")], neuper@38037: calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")), neuper@38037: ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")), wneuper@59360: ("DIVIDE",("Rings.divide_class.divide", neuper@38037: eval_cancel "#divide_e")), neuper@38037: ("POWER" ,("Atools.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}; neuper@42398: *} neuper@37950: neuper@42398: text {* 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" neuper@42398: *} neuper@42398: ML {* 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_, wneuper@59416: 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: }; neuper@48763: *} neuper@48763: ML {* 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_, wneuper@59416: 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: }; neuper@48763: *} neuper@48763: ML {* 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*) wneuper@59416: 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: }; neuper@48763: *} neuper@48763: ML {* 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, neuper@38014: calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37950: ("POWER", ("Atools.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: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.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: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.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}; neuper@48763: *} neuper@52125: wneuper@59374: ML {* val prep_rls' = LTool.prep_rls @{theory} *} s1210629013@55444: neuper@52125: setup {* 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", s1210629013@55444: (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))] *} s1210629013@52145: setup {* KEStore_Elems.add_calcs s1210629013@52145: [("is_polyrat_in", ("Poly.is'_polyrat'_in", s1210629013@52145: eval_is_polyrat_in "#eval_is_polyrat_in")), s1210629013@52145: ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")), s1210629013@52145: ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")), s1210629013@52145: ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")), s1210629013@52145: ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")), s1210629013@52145: ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")), s1210629013@52145: ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))] *} s1210629013@52145: neuper@37950: (** problems **) s1210629013@55359: setup {* 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", s1210629013@55339: [["simplification","for_polynomials"]]))] *} wneuper@59429: neuper@37950: (** methods **) wneuper@59429: (*----- wneuper@59429: consts wneuper@59429: norm_Poly :: ID wneuper@59429: partial_function (tailrec) simplify :: "real \ real" wneuper@59429: where wneuper@59429: "simplify term = ((Rewrite_Set norm_Poly False) term)" wneuper@59429: wneuper@59429: -----*) s1210629013@55373: setup {* KEStore_Elems.add_mets wneuper@59406: [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_*) wneuper@59416: Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")], wneuper@59416: crls = Rule.e_rls, errpats = [], nrls = norm_Poly}, s1210629013@55373: "Script SimplifyScript (t_t::real) = " ^ s1210629013@55373: " ((Rewrite_Set norm_Poly False) t_t)")] s1210629013@55373: *} neuper@37950: wneuper@59429: ML {* wneuper@59429: *} ML {* wneuper@59429: *} neuper@37906: end