1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/IsacKnowledge/Poly.ML Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,1495 @@
1.4 +(*.eval_funs, rulesets, problems and methods concerning polynamials
1.5 + authors: Matthias Goldgruber 2003
1.6 + (c) due to copyright terms
1.7 +
1.8 + use"../IsacKnowledge/Poly.ML";
1.9 + use"IsacKnowledge/Poly.ML";
1.10 + use"Poly.ML";
1.11 +
1.12 + remove_thy"Poly";
1.13 + use_thy"IsacKnowledge/Isac";
1.14 +****************************************************************.*)
1.15 +
1.16 +(*.****************************************************************
1.17 + remark on 'polynomials'
1.18 + WN020919
1.19 + there are 5 kinds of expanded normalforms:
1.20 +[1] 'complete polynomial' (Komplettes Polynom), univariate
1.21 + a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
1.22 + not (a_n = 0), some a_i may be zero (DON'T disappear),
1.23 + variables in monomials lexicographically ordered and complete,
1.24 + x written as 1*x^1, ...
1.25 +[2] 'polynomial' (Polynom), univariate and multivariate
1.26 + a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
1.27 + 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
1.28 + not (a_n = 0), some a_i may be zero (ie. monomials disappear),
1.29 + exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
1.30 + and variables in monomials are lexicographically ordered
1.31 + examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
1.32 + [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
1.33 + [2]: "x + (-50) * x ^^^ 3"
1.34 + [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
1.35 +
1.36 +[3] 'expanded_term' (Ausmultiplizierter Term):
1.37 + pull out unary minus to binary minus,
1.38 + as frequently exercised in schools; other conditions for [2] hold however
1.39 + examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
1.40 + "4 * x ^^^ 2 - 9 * y ^^^ 2"
1.41 +[4] 'polynomial_in' (Polynom in):
1.42 + polynomial in 1 variable with arbitrary coefficients
1.43 + examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
1.44 + "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
1.45 +[5] 'expanded_in' (Ausmultiplizierter Termin in):
1.46 + analoguous to [3] with binary minus like [3]
1.47 + examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
1.48 + "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
1.49 +*****************************************************************.*)
1.50 +
1.51 +"******** Poly.ML begin ******************************************";
1.52 +theory' := overwritel (!theory', [("Poly.thy",Poly.thy)]);
1.53 +
1.54 +
1.55 +(* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
1.56 +fun is_polyrat_in t v =
1.57 + let
1.58 + fun coeff_in c v = v mem (vars c);
1.59 + fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
1.60 + (* at the moment there is no term like this, but ....*)
1.61 + | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = not(coeff_in b v)
1.62 + | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) orelse (finddivide t2 v)
1.63 + | finddivide (_ $ t1) v = (finddivide t1 v)
1.64 + | finddivide _ _ = false;
1.65 + in
1.66 + finddivide t v
1.67 + end;
1.68 +
1.69 +fun eval_is_polyrat_in _ _ (p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
1.70 + if is_polyrat_in t v then
1.71 + Some ((term2str p) ^ " = True",
1.72 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.73 + else Some ((term2str p) ^ " = True",
1.74 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.75 + | eval_is_polyrat_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);
1.76 +
1.77 +
1.78 +local
1.79 + (*.a 'c is coefficient of v' if v does NOT occur in c.*)
1.80 + fun coeff_in c v = not (v mem (vars c));
1.81 + (*
1.82 + val v = (term_of o the o (parse thy)) "x";
1.83 + val t = (term_of o the o (parse thy)) "1";
1.84 + coeff_in t v;
1.85 + (*val it = true : bool*)
1.86 + val t = (term_of o the o (parse thy)) "a*b+c";
1.87 + coeff_in t v;
1.88 + (*val it = true : bool*)
1.89 + val t = (term_of o the o (parse thy)) "a*x+c";
1.90 + coeff_in t v;
1.91 + (*val it = false : bool*)
1.92 + *)
1.93 + (*. a 'monomial t in variable v' is a term t with
1.94 + either (1) v NOT existent in t, or (2) v contained in t,
1.95 + if (1) then degree 0
1.96 + if (2) then v is a factor on the very right, ev. with exponent.*)
1.97 + fun factor_right_deg (*case 2*)
1.98 + (t as Const ("op *",_) $ t1 $
1.99 + (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
1.100 + if ((vv = v) andalso (coeff_in t1 v)) then Some (int_of_str' d) else None
1.101 + | factor_right_deg
1.102 + (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
1.103 + if (vv = v) then Some (int_of_str' d) else None
1.104 + | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
1.105 + if ((vv = v) andalso (coeff_in t1 v))then Some 1 else None
1.106 + | factor_right_deg vv v =
1.107 + if (vv = v) then Some 1 else None;
1.108 + fun mono_deg_in m v =
1.109 + if coeff_in m v then (*case 1*) Some 0
1.110 + else factor_right_deg m v;
1.111 + (*
1.112 + val v = (term_of o the o (parse thy)) "x";
1.113 + val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
1.114 + mono_deg_in t v;
1.115 + (*val it = Some 7*)
1.116 + val t = (term_of o the o (parse thy)) "x^^^7";
1.117 + mono_deg_in t v;
1.118 + (*val it = Some 7*)
1.119 + val t = (term_of o the o (parse thy)) "(a*b+c)*x";
1.120 + mono_deg_in t v;
1.121 + (*val it = Some 1*)
1.122 + val t = (term_of o the o (parse thy)) "(a*b+x)*x";
1.123 + mono_deg_in t v;
1.124 + (*val it = None*)
1.125 + val t = (term_of o the o (parse thy)) "x";
1.126 + mono_deg_in t v;
1.127 + (*val it = Some 1*)
1.128 + val t = (term_of o the o (parse thy)) "(a*b+c)";
1.129 + mono_deg_in t v;
1.130 + (*val it = Some 0*)
1.131 + val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
1.132 + mono_deg_in t v;
1.133 + (*val it = None*)
1.134 + *)
1.135 + fun expand_deg_in t v =
1.136 + let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.137 + (case mono_deg_in t2 v of (* $ is left associative*)
1.138 + Some d' => edi d' d' t1
1.139 + | None => None)
1.140 + | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
1.141 + (case mono_deg_in t2 v of
1.142 + Some d' => edi d' d' t1
1.143 + | None => None)
1.144 + | edi d dmax (Const ("op -",_) $ t1 $ t2) =
1.145 + (case mono_deg_in t2 v of
1.146 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.147 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.148 + | None => None)
1.149 + | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.150 + (case mono_deg_in t2 v of
1.151 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.152 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.153 + | None => None)
1.154 + | edi ~1 ~1 t =
1.155 + (case mono_deg_in t v of
1.156 + d as Some _ => d
1.157 + | None => None)
1.158 + | edi d dmax t = (*basecase last*)
1.159 + (case mono_deg_in t v of
1.160 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then Some dmax else None
1.161 + | None => None)
1.162 + in edi ~1 ~1 t end;
1.163 + (*
1.164 + val v = (term_of o the o (parse thy)) "x";
1.165 + val t = (term_of o the o (parse thy)) "a+b";
1.166 + expand_deg_in t v;
1.167 + (*val it = Some 0*)
1.168 + val t = (term_of o the o (parse thy)) "(a+b)*x";
1.169 + expand_deg_in t v;
1.170 + (*Some 1*)
1.171 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
1.172 + expand_deg_in t v;
1.173 + (*Some 1*)
1.174 + val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
1.175 + expand_deg_in t v;
1.176 + (*Some 1*)
1.177 + val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
1.178 + expand_deg_in t v;
1.179 + *)
1.180 + fun poly_deg_in t v =
1.181 + let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.182 + (case mono_deg_in t2 v of (* $ is left associative*)
1.183 + Some d' => edi d' d' t1
1.184 + | None => None)
1.185 + | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.186 + (case mono_deg_in t2 v of
1.187 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.188 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.189 + | None => None)
1.190 + | edi ~1 ~1 t =
1.191 + (case mono_deg_in t v of
1.192 + d as Some _ => d
1.193 + | None => None)
1.194 + | edi d dmax t = (*basecase last*)
1.195 + (case mono_deg_in t v of
1.196 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then Some dmax else None
1.197 + | None => None)
1.198 + in edi ~1 ~1 t end;
1.199 +in
1.200 +
1.201 +fun is_expanded_in t v =
1.202 + case expand_deg_in t v of Some _ => true | None => false;
1.203 +fun is_poly_in t v =
1.204 + case poly_deg_in t v of Some _ => true | None => false;
1.205 +fun has_degree_in t v =
1.206 + case expand_deg_in t v of Some d => d | None => ~1;
1.207 +end;
1.208 +(*
1.209 + val v = (term_of o the o (parse thy)) "x";
1.210 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
1.211 + has_degree_in t v;
1.212 + (*val it = 2*)
1.213 + val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
1.214 + has_degree_in t v;
1.215 + (*val it = 2*)
1.216 + val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
1.217 + has_degree_in t v;
1.218 + (*val it = 2*)
1.219 +*)
1.220 +
1.221 +(*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
1.222 +fun eval_is_expanded_in _ _
1.223 + (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
1.224 + if is_expanded_in t v
1.225 + then Some ((term2str p) ^ " = True",
1.226 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.227 + else Some ((term2str p) ^ " = True",
1.228 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.229 + | eval_is_expanded_in _ _ _ _ = None;
1.230 +(*
1.231 + val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.232 + val Some (id, t') = eval_is_expanded_in 0 0 t 0;
1.233 + (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
1.234 + term2str t';
1.235 + (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
1.236 +*)
1.237 +(*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
1.238 +fun eval_is_poly_in _ _
1.239 + (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
1.240 + if is_poly_in t v
1.241 + then Some ((term2str p) ^ " = True",
1.242 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.243 + else Some ((term2str p) ^ " = True",
1.244 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.245 + | eval_is_poly_in _ _ _ _ = None;
1.246 +(*
1.247 + val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
1.248 + val Some (id, t') = eval_is_poly_in 0 0 t 0;
1.249 + (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
1.250 + term2str t';
1.251 + (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
1.252 +*)
1.253 +
1.254 +(*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
1.255 +fun eval_has_degree_in _ _
1.256 + (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
1.257 + let val d = has_degree_in t v
1.258 + val d' = term_of_num HOLogic.realT d
1.259 + in Some ((term2str p) ^ " = " ^ (string_of_int d),
1.260 + Trueprop $ (mk_equality (p, d')))
1.261 + end
1.262 + | eval_has_degree_in _ _ _ _ = None;
1.263 +(*
1.264 +> val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
1.265 +> val Some (id, t') = eval_has_degree_in 0 0 t 0;
1.266 +val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
1.267 +> term2str t';
1.268 +val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
1.269 +*)
1.270 +
1.271 +(*..*)
1.272 +val calculate_Poly =
1.273 + append_rls "calculate_PolyFIXXXME.not.impl." e_rls
1.274 + [];
1.275 +
1.276 +(*.for evaluation of conditions in rewrite rules.*)
1.277 +val Poly_erls =
1.278 + append_rls "Poly_erls" Atools_erls
1.279 + [ Calc ("op =",eval_equal "#equal_"),
1.280 + Thm ("real_unari_minus",num_str real_unari_minus),
1.281 + Calc ("op +",eval_binop "#add_"),
1.282 + Calc ("op -",eval_binop "#sub_"),
1.283 + Calc ("op *",eval_binop "#mult_"),
1.284 + Calc ("Atools.pow" ,eval_binop "#power_")
1.285 + ];
1.286 +
1.287 +val poly_crls =
1.288 + append_rls "poly_crls" Atools_crls
1.289 + [ Calc ("op =",eval_equal "#equal_"),
1.290 + Thm ("real_unari_minus",num_str real_unari_minus),
1.291 + Calc ("op +",eval_binop "#add_"),
1.292 + Calc ("op -",eval_binop "#sub_"),
1.293 + Calc ("op *",eval_binop "#mult_"),
1.294 + Calc ("Atools.pow" ,eval_binop "#power_")
1.295 + ];
1.296 +
1.297 +
1.298 +local (*. for make_polynomial .*)
1.299 +
1.300 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.301 +
1.302 +fun pr_ord EQUAL = "EQUAL"
1.303 + | pr_ord LESS = "LESS"
1.304 + | pr_ord GREATER = "GREATER";
1.305 +
1.306 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.307 + (case a of
1.308 + "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
1.309 + | _ => (((a, 0), T), 0))
1.310 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.311 + | dest_hd' (Var v) = (v, 2)
1.312 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.313 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.314 +
1.315 +fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
1.316 + (case int_of_str (order) of
1.317 + Some d => d
1.318 + | None => 0)
1.319 + | get_order_pow _ = 0;
1.320 +
1.321 +fun size_of_term' (Const(str,_) $ t) =
1.322 + if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
1.323 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.324 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.325 + | size_of_term' _ = 1;
1.326 +
1.327 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.328 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.329 + | term_ord' pr thy (t, u) =
1.330 + (if pr then
1.331 + let
1.332 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.333 + val _=writeln("t= f@ts= \""^
1.334 + ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
1.335 + (commas(map(string_of_cterm o cterm_of (sign_of thy))ts))^"]\"");
1.336 + val _=writeln("u= g@us= \""^
1.337 + ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
1.338 + (commas(map(string_of_cterm o cterm_of (sign_of thy))us))^"]\"");
1.339 + val _=writeln("size_of_term(t,u)= ("^
1.340 + (string_of_int(size_of_term' t))^", "^
1.341 + (string_of_int(size_of_term' u))^")");
1.342 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
1.343 + val _=writeln("terms_ord(ts,us) = "^
1.344 + ((pr_ord o terms_ord str false)(ts,us)));
1.345 + val _=writeln("-------");
1.346 + in () end
1.347 + else ();
1.348 + case int_ord (size_of_term' t, size_of_term' u) of
1.349 + EQUAL =>
1.350 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.351 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.352 + | ord => ord)
1.353 + end
1.354 + | ord => ord)
1.355 +and hd_ord (f, g) = (* ~ term.ML *)
1.356 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.357 +and terms_ord str pr (ts, us) =
1.358 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.359 +in
1.360 +
1.361 +fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
1.362 + (term_ord' pr thy(***) tu = LESS );
1.363 +
1.364 +end;(*local*)
1.365 +
1.366 +
1.367 +rew_ord' := overwritel (!rew_ord',
1.368 +[("termlessI", termlessI),
1.369 + ("ord_make_polynomial", ord_make_polynomial false thy)
1.370 + ]);
1.371 +
1.372 +
1.373 +val expand =
1.374 + Rls{id = "expand", preconds = [],
1.375 + rew_ord = ("dummy_ord", dummy_ord),
1.376 + erls = e_rls,srls = Erls,
1.377 + calc = [],
1.378 + (*asm_thm = [],*)
1.379 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.380 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.381 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2)
1.382 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.383 + ], scr = EmptyScr}:rls;
1.384 +
1.385 +(*----------------- Begin: rulesets for make_polynomial_ -----------------
1.386 + 'rlsIDs' redefined by MG as 'rlsIDs_'
1.387 + ^^^*)
1.388 +
1.389 +val discard_minus_ =
1.390 + Rls{id = "discard_minus_", preconds = [],
1.391 + rew_ord = ("dummy_ord", dummy_ord),
1.392 + erls = e_rls,srls = Erls,
1.393 + calc = [],
1.394 + (*asm_thm = [],*)
1.395 + rules = [Thm ("real_diff_minus",num_str real_diff_minus),
1.396 + (*"a - b = a + -1 * b"*)
1.397 + Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.398 + (*- ?z = "-1 * ?z"*)
1.399 + ], scr = EmptyScr}:rls;
1.400 +val expand_poly_ =
1.401 + Rls{id = "expand_poly_", preconds = [],
1.402 + rew_ord = ("dummy_ord", dummy_ord),
1.403 + erls = e_rls,srls = Erls,
1.404 + calc = [],
1.405 + (*asm_thm = [],*)
1.406 + rules = [Thm ("real_plus_binom_pow4",num_str real_plus_binom_pow4),
1.407 + (*"(a + b)^^^4 = ... "*)
1.408 + Thm ("real_plus_binom_pow5",num_str real_plus_binom_pow5),
1.409 + (*"(a + b)^^^5 = ... "*)
1.410 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.411 + (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.412 +
1.413 + (*WN071229 changed/removed for Schaerding -----vvv*)
1.414 + (*Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),*)
1.415 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.416 + Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.417 + (*"(a + b)^^^2 = (a + b) * (a + b)"*)
1.418 + (*Thm ("real_plus_minus_binom1_p_p",
1.419 + num_str real_plus_minus_binom1_p_p),*)
1.420 + (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.421 + (*Thm ("real_plus_minus_binom2_p_p",
1.422 + num_str real_plus_minus_binom2_p_p),*)
1.423 + (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.424 + (*WN071229 changed/removed for Schaerding -----^^^*)
1.425 +
1.426 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.427 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.428 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.429 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.430 +
1.431 + Thm ("realpow_multI", num_str realpow_multI),
1.432 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.433 + Thm ("realpow_pow",num_str realpow_pow)
1.434 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.435 + ], scr = EmptyScr}:rls;
1.436 +
1.437 +(*.the expression contains + - * ^ only ?
1.438 + this is weaker than 'is_polynomial' !.*)
1.439 +fun is_polyexp (Free _) = true
1.440 + | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
1.441 + | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
1.442 + | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
1.443 + | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.444 + | is_polyexp (Const ("op +",_) $ t1 $ t2) =
1.445 + ((is_polyexp t1) andalso (is_polyexp t2))
1.446 + | is_polyexp (Const ("op -",_) $ t1 $ t2) =
1.447 + ((is_polyexp t1) andalso (is_polyexp t2))
1.448 + | is_polyexp (Const ("op *",_) $ t1 $ t2) =
1.449 + ((is_polyexp t1) andalso (is_polyexp t2))
1.450 + | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
1.451 + ((is_polyexp t1) andalso (is_polyexp t2))
1.452 + | is_polyexp _ = false;
1.453 +
1.454 +(*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
1.455 +fun eval_is_polyexp (thmid:string) _
1.456 + (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
1.457 + if is_polyexp arg
1.458 + then Some (mk_thmid thmid ""
1.459 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.460 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.461 + else Some (mk_thmid thmid ""
1.462 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.463 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.464 + | eval_is_polyexp _ _ _ _ = None;
1.465 +
1.466 +val expand_poly_rat_ =
1.467 + Rls{id = "expand_poly_rat_", preconds = [],
1.468 + rew_ord = ("dummy_ord", dummy_ord),
1.469 + erls = append_rls "e_rls-is_polyexp" e_rls
1.470 + [Calc ("Poly.is'_polyexp", eval_is_polyexp "")
1.471 + ],
1.472 + srls = Erls,
1.473 + calc = [],
1.474 + (*asm_thm = [],*)
1.475 + rules = [Thm ("real_plus_binom_pow4_poly",num_str real_plus_binom_pow4_poly),
1.476 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
1.477 + Thm ("real_plus_binom_pow5_poly",num_str real_plus_binom_pow5_poly),
1.478 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
1.479 + Thm ("real_plus_binom_pow2_poly",num_str real_plus_binom_pow2_poly),
1.480 + (*"[| a is_polyexp; b is_polyexp |] ==>
1.481 + (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.482 + Thm ("real_plus_binom_pow3_poly",num_str real_plus_binom_pow3_poly),
1.483 + (*"[| a is_polyexp; b is_polyexp |] ==>
1.484 + (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.485 + Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
1.486 + (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.487 + Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
1.488 + (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.489 +
1.490 + Thm ("real_add_mult_distrib_poly" ,num_str real_add_mult_distrib_poly),
1.491 + (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.492 + Thm ("real_add_mult_distrib2_poly",num_str real_add_mult_distrib2_poly),
1.493 + (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.494 +
1.495 + Thm ("realpow_multI_poly", num_str realpow_multI_poly),
1.496 + (*"[| r is_polyexp; s is_polyexp |] ==>
1.497 + (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.498 + Thm ("realpow_pow",num_str realpow_pow)
1.499 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.500 + ], scr = EmptyScr}:rls;
1.501 +
1.502 +val simplify_power_ =
1.503 + Rls{id = "simplify_power_", preconds = [],
1.504 + rew_ord = ("dummy_ord", dummy_ord),
1.505 + erls = e_rls, srls = Erls,
1.506 + calc = [],
1.507 + (*asm_thm = [],*)
1.508 + rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.509 + a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
1.510 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.511 + (*"r * r = r ^^^ 2"*)
1.512 + Thm ("realpow_twoI_assoc_l",num_str realpow_twoI_assoc_l),
1.513 + (*"r * (r * s) = r ^^^ 2 * s"*)
1.514 +
1.515 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.516 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.517 + Thm ("realpow_plus_1_assoc_l", num_str realpow_plus_1_assoc_l),
1.518 + (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
1.519 + (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
1.520 + Thm ("realpow_plus_1_assoc_l2", num_str realpow_plus_1_assoc_l2),
1.521 + (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
1.522 +
1.523 + Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.524 + (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.525 + Thm ("realpow_addI_assoc_l", num_str realpow_addI_assoc_l),
1.526 + (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
1.527 +
1.528 + (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
1.529 + "r * r = r ^^^ 2" wenn r=a^^^b*)
1.530 + Thm ("realpow_pow",num_str realpow_pow)
1.531 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.532 + ], scr = EmptyScr}:rls;
1.533 +
1.534 +val calc_add_mult_pow_ =
1.535 + Rls{id = "calc_add_mult_pow_", preconds = [],
1.536 + rew_ord = ("dummy_ord", dummy_ord),
1.537 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.538 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.539 + ("times" , ("op *", eval_binop "#mult_")),
1.540 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.541 + ],
1.542 + (*asm_thm = [],*)
1.543 + rules = [Calc ("op +", eval_binop "#add_"),
1.544 + Calc ("op *", eval_binop "#mult_"),
1.545 + Calc ("Atools.pow", eval_binop "#power_")
1.546 + ], scr = EmptyScr}:rls;
1.547 +
1.548 +val reduce_012_mult_ =
1.549 + Rls{id = "reduce_012_mult_", preconds = [],
1.550 + rew_ord = ("dummy_ord", dummy_ord),
1.551 + erls = e_rls,srls = Erls,
1.552 + calc = [],
1.553 + (*asm_thm = [],*)
1.554 + rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
1.555 + Thm ("real_mult_1_right",num_str real_mult_1_right),
1.556 + (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
1.557 + Thm ("realpow_zeroI",num_str realpow_zeroI),
1.558 + (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
1.559 + Thm ("realpow_oneI",num_str realpow_oneI),
1.560 + (*"r ^^^ 1 = r"*)
1.561 + Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.562 + (*"1 ^^^ n = 1"*)
1.563 + ], scr = EmptyScr}:rls;
1.564 +
1.565 +val collect_numerals_ =
1.566 + Rls{id = "collect_numerals_", preconds = [],
1.567 + rew_ord = ("dummy_ord", dummy_ord),
1.568 + erls = Atools_erls, srls = Erls,
1.569 + calc = [("plus" , ("op +", eval_binop "#add_"))
1.570 + ],
1.571 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.572 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.573 + Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
1.574 + (*"[| l is_const; m is_const |] ==> \
1.575 + \(k + m * n) + l * n = k + (l + m)*n"*)
1.576 + Thm ("real_one_collect",num_str real_one_collect),
1.577 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.578 + Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
1.579 + (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.580 +
1.581 + Calc ("op +", eval_binop "#add_"),
1.582 +
1.583 + (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.584 + (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.585 + Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
1.586 + (*"(k + z1) + z1 = k + 2 * z1"*)
1.587 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
1.588 + (*"z1 + z1 = 2 * z1"*)
1.589 +
1.590 + ], scr = EmptyScr}:rls;
1.591 +
1.592 +val reduce_012_ =
1.593 + Rls{id = "reduce_012_", preconds = [],
1.594 + rew_ord = ("dummy_ord", dummy_ord),
1.595 + erls = e_rls,srls = Erls,
1.596 + calc = [],
1.597 + (*asm_thm = [],*)
1.598 + rules = [Thm ("real_mult_1",num_str real_mult_1),
1.599 + (*"1 * z = z"*)
1.600 + Thm ("real_mult_0",num_str real_mult_0),
1.601 + (*"0 * z = 0"*)
1.602 + Thm ("real_mult_0_right",num_str real_mult_0_right),
1.603 + (*"z * 0 = 0"*)
1.604 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.605 + (*"0 + z = z"*)
1.606 + Thm ("real_add_zero_right",num_str real_add_zero_right),
1.607 + (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
1.608 +
1.609 + (*Thm ("realpow_oneI",num_str realpow_oneI)*)
1.610 + (*"?r ^^^ 1 = ?r"*)
1.611 + Thm ("real_0_divide",num_str real_0_divide)(*WN060914*)
1.612 + (*"0 / ?x = 0"*)
1.613 + ], scr = EmptyScr}:rls;
1.614 +
1.615 +(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.616 +val discard_parentheses_ =
1.617 + append_rls "discard_parentheses_" e_rls
1.618 + [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
1.619 + (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
1.620 + (*Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))*)
1.621 + (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
1.622 + ];
1.623 +
1.624 +(*----------------- End: rulesets for make_polynomial_ -----------------*)
1.625 +
1.626 +(*MG.0401 ev. for use in rls with ordered rewriting ?
1.627 +val collect_numerals_left =
1.628 + Rls{id = "collect_numerals", preconds = [],
1.629 + rew_ord = ("dummy_ord", dummy_ord),
1.630 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.631 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.632 + ("times" , ("op *", eval_binop "#mult_")),
1.633 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.634 + ],
1.635 + (*asm_thm = [],*)
1.636 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.637 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.638 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.639 + (*"[| l is_const; m is_const |] ==>
1.640 + l * n + (m * n + k) = (l + m) * n + k"*)
1.641 + Thm ("real_one_collect",num_str real_one_collect),
1.642 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.643 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.644 + (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
1.645 +
1.646 + Calc ("op +", eval_binop "#add_"),
1.647 +
1.648 + (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
1.649 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.650 + (*"z1 + z1 = 2 * z1"*)
1.651 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.652 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.653 + ], scr = EmptyScr}:rls;*)
1.654 +
1.655 +val expand_poly =
1.656 + Rls{id = "expand_poly", preconds = [],
1.657 + rew_ord = ("dummy_ord", dummy_ord),
1.658 + erls = e_rls,srls = Erls,
1.659 + calc = [],
1.660 + (*asm_thm = [],*)
1.661 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.662 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.663 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.664 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.665 + (*Thm ("real_add_mult_distrib1",num_str real_add_mult_distrib1),
1.666 + ....... 18.3.03 undefined???*)
1.667 +
1.668 + Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.669 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.670 + Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p),
1.671 + (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
1.672 + Thm ("real_plus_minus_binom1_p",
1.673 + num_str real_plus_minus_binom1_p),
1.674 + (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
1.675 + Thm ("real_plus_minus_binom2_p",
1.676 + num_str real_plus_minus_binom2_p),
1.677 + (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.678 +
1.679 + Thm ("real_minus_minus",num_str real_minus_minus),
1.680 + (*"- (- ?z) = ?z"*)
1.681 + Thm ("real_diff_minus",num_str real_diff_minus),
1.682 + (*"a - b = a + -1 * b"*)
1.683 + Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.684 + (*- ?z = "-1 * ?z"*)
1.685 +
1.686 + (*Thm ("",num_str ),
1.687 + Thm ("",num_str ),
1.688 + Thm ("",num_str ),*)
1.689 + (*Thm ("real_minus_add_distrib",
1.690 + num_str real_minus_add_distrib),*)
1.691 + (*"- (?x + ?y) = - ?x + - ?y"*)
1.692 + (*Thm ("real_diff_plus",num_str real_diff_plus)*)
1.693 + (*"a - b = a + -b"*)
1.694 + ], scr = EmptyScr}:rls;
1.695 +val simplify_power =
1.696 + Rls{id = "simplify_power", preconds = [],
1.697 + rew_ord = ("dummy_ord", dummy_ord),
1.698 + erls = e_rls, srls = Erls,
1.699 + calc = [],
1.700 + (*asm_thm = [],*)
1.701 + rules = [Thm ("realpow_multI", num_str realpow_multI),
1.702 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.703 +
1.704 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.705 + (*"r1 * r1 = r1 ^^^ 2"*)
1.706 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.707 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.708 + Thm ("realpow_pow",num_str realpow_pow),
1.709 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.710 + Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.711 + (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.712 + Thm ("realpow_oneI",num_str realpow_oneI),
1.713 + (*"r ^^^ 1 = r"*)
1.714 + Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.715 + (*"1 ^^^ n = 1"*)
1.716 + ], scr = EmptyScr}:rls;
1.717 +(*MG.0401: termorders for multivariate polys dropped due to principal problems:
1.718 + (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1.719 +val order_add_mult =
1.720 + Rls{id = "order_add_mult", preconds = [],
1.721 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.722 + erls = e_rls,srls = Erls,
1.723 + calc = [],
1.724 + (*asm_thm = [],*)
1.725 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.726 + (* z * w = w * z *)
1.727 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.728 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.729 + Thm ("real_mult_assoc",num_str real_mult_assoc),
1.730 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.731 + Thm ("real_add_commute",num_str real_add_commute),
1.732 + (*z + w = w + z*)
1.733 + Thm ("real_add_left_commute",num_str real_add_left_commute),
1.734 + (*x + (y + z) = y + (x + z)*)
1.735 + Thm ("real_add_assoc",num_str real_add_assoc)
1.736 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.737 + ], scr = EmptyScr}:rls;
1.738 +(*MG.0401: termorders for multivariate polys dropped due to principal problems:
1.739 + (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1.740 +val order_mult =
1.741 + Rls{id = "order_mult", preconds = [],
1.742 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.743 + erls = e_rls,srls = Erls,
1.744 + calc = [],
1.745 + (*asm_thm = [],*)
1.746 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.747 + (* z * w = w * z *)
1.748 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.749 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.750 + Thm ("real_mult_assoc",num_str real_mult_assoc)
1.751 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.752 + ], scr = EmptyScr}:rls;
1.753 +val collect_numerals =
1.754 + Rls{id = "collect_numerals", preconds = [],
1.755 + rew_ord = ("dummy_ord", dummy_ord),
1.756 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.757 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.758 + ("times" , ("op *", eval_binop "#mult_")),
1.759 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.760 + ],
1.761 + (*asm_thm = [],*)
1.762 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.763 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.764 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.765 + (*"[| l is_const; m is_const |] ==>
1.766 + l * n + (m * n + k) = (l + m) * n + k"*)
1.767 + Thm ("real_one_collect",num_str real_one_collect),
1.768 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.769 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.770 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.771 + Calc ("op +", eval_binop "#add_"),
1.772 + Calc ("op *", eval_binop "#mult_"),
1.773 + Calc ("Atools.pow", eval_binop "#power_")
1.774 + ], scr = EmptyScr}:rls;
1.775 +val reduce_012 =
1.776 + Rls{id = "reduce_012", preconds = [],
1.777 + rew_ord = ("dummy_ord", dummy_ord),
1.778 + erls = e_rls,srls = Erls,
1.779 + calc = [],
1.780 + (*asm_thm = [],*)
1.781 + rules = [Thm ("real_mult_1",num_str real_mult_1),
1.782 + (*"1 * z = z"*)
1.783 + (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
1.784 + (*"-1 * z = - z"*)
1.785 + Thm ("sym_real_mult_minus_eq1",
1.786 + num_str (real_mult_minus_eq1 RS sym)),
1.787 + (*- (?x * ?y) = "- ?x * ?y"*)
1.788 + (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
1.789 + (*"- ?x * - ?y = ?x * ?y"*)---*)
1.790 + Thm ("real_mult_0",num_str real_mult_0),
1.791 + (*"0 * z = 0"*)
1.792 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.793 + (*"0 + z = z"*)
1.794 + Thm ("real_add_minus",num_str real_add_minus),
1.795 + (*"?z + - ?z = 0"*)
1.796 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.797 + (*"z1 + z1 = 2 * z1"*)
1.798 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.799 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.800 + ], scr = EmptyScr}:rls;
1.801 +(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.802 +val discard_parentheses =
1.803 + append_rls "discard_parentheses" e_rls
1.804 + [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)),
1.805 + Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))];
1.806 +
1.807 +val scr_make_polynomial =
1.808 +"Script Expand_binoms t_ =\
1.809 +\(Repeat \
1.810 +\((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.811 +
1.812 +\ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \
1.813 +\ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \
1.814 +\ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \
1.815 +\ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \
1.816 +
1.817 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.818 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.819 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.820 +
1.821 +\ (Try (Repeat (Rewrite real_mult_commute False))) @@ \
1.822 +\ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \
1.823 +\ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \
1.824 +\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.825 +\ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \
1.826 +\ (Try (Repeat (Rewrite real_add_assoc False))) @@ \
1.827 +
1.828 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.829 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.830 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.831 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.832 +
1.833 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.834 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.835 +
1.836 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.837 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.838 +
1.839 +\ (Try (Repeat (Calculate plus ))) @@ \
1.840 +\ (Try (Repeat (Calculate times ))) @@ \
1.841 +\ (Try (Repeat (Calculate power_)))) \
1.842 +\ t_)";
1.843 +
1.844 +(*version used by MG.02/03, overwritten by version AG in 04 below
1.845 +val make_polynomial = prep_rls(
1.846 + Seq{id = "make_polynomial", preconds = []:term list,
1.847 + rew_ord = ("dummy_ord", dummy_ord),
1.848 + erls = Atools_erls, srls = Erls,
1.849 + calc = [],(*asm_thm = [],*)
1.850 + rules = [Rls_ expand_poly,
1.851 + Rls_ order_add_mult,
1.852 + Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
1.853 + Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
1.854 + Rls_ reduce_012,
1.855 + Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
1.856 + Rls_ discard_parentheses
1.857 + ],
1.858 + scr = EmptyScr
1.859 + }:rls); *)
1.860 +
1.861 +val scr_expand_binoms =
1.862 +"Script Expand_binoms t_ =\
1.863 +\(Repeat \
1.864 +\((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \
1.865 +\ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \
1.866 +\ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \
1.867 +\ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \
1.868 +\ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \
1.869 +\ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \
1.870 +
1.871 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.872 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.873 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.874 +
1.875 +\ (Try (Repeat (Calculate plus ))) @@ \
1.876 +\ (Try (Repeat (Calculate times ))) @@ \
1.877 +\ (Try (Repeat (Calculate power_))) @@ \
1.878 +
1.879 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.880 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.881 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.882 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.883 +
1.884 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.885 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.886 +
1.887 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.888 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.889 +
1.890 +\ (Try (Repeat (Calculate plus ))) @@ \
1.891 +\ (Try (Repeat (Calculate times ))) @@ \
1.892 +\ (Try (Repeat (Calculate power_)))) \
1.893 +\ t_)";
1.894 +
1.895 +val expand_binoms =
1.896 + Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.897 + erls = Atools_erls, srls = Erls,
1.898 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.899 + ("times" , ("op *", eval_binop "#mult_")),
1.900 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.901 + ],
1.902 + (*asm_thm = [],*)
1.903 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.904 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.905 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.906 + (*"(a + b)*(a + b) = ...*)
1.907 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.908 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.909 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.910 + (*"(a - b)*(a - b) = ...*)
1.911 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.912 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.913 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.914 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.915 + (*RL 020915*)
1.916 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.917 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.918 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.919 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.920 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.921 + (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1.922 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.923 + (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1.924 + Thm ("realpow_multI",num_str realpow_multI),
1.925 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.926 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.927 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.928 + Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.929 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.930 +
1.931 +
1.932 + (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.933 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.934 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.935 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.936 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.937 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.938 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.939 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.940 + *)
1.941 +
1.942 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
1.943 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
1.944 + Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
1.945 +
1.946 + Calc ("op +", eval_binop "#add_"),
1.947 + Calc ("op *", eval_binop "#mult_"),
1.948 + Calc ("Atools.pow", eval_binop "#power_"),
1.949 + (*
1.950 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.951 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.952 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.953 + Thm ("real_add_commute",num_str real_add_commute), (**)
1.954 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
1.955 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
1.956 + *)
1.957 +
1.958 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.959 + (*"r1 * r1 = r1 ^^^ 2"*)
1.960 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.961 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.962 + (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.963 + (*"z1 + z1 = 2 * z1"*)*)
1.964 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.965 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.966 +
1.967 + Thm ("real_num_collect",num_str real_num_collect),
1.968 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.969 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.970 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.971 + Thm ("real_one_collect",num_str real_one_collect),
1.972 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.973 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.974 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.975 +
1.976 + Calc ("op +", eval_binop "#add_"),
1.977 + Calc ("op *", eval_binop "#mult_"),
1.978 + Calc ("Atools.pow", eval_binop "#power_")
1.979 + ],
1.980 + scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
1.981 + }:rls;
1.982 +
1.983 +
1.984 +"******* Poly.ML end ******* ...RL";
1.985 +
1.986 +
1.987 +(**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
1.988 +
1.989 +(*FIXME.0401: make SML-order local to make_polynomial(_) *)
1.990 +(*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1.991 +(* Polynom --> List von Monomen *)
1.992 +fun poly2list (Const ("op +",_) $ t1 $ t2) =
1.993 + (poly2list t1) @ (poly2list t2)
1.994 + | poly2list t = [t];
1.995 +
1.996 +(* Monom --> Liste von Variablen *)
1.997 +fun monom2list (Const ("op *",_) $ t1 $ t2) =
1.998 + (monom2list t1) @ (monom2list t2)
1.999 + | monom2list t = [t];
1.1000 +
1.1001 +(* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1.1002 +fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1.1003 + | get_basStr (Free (str, _)) = str
1.1004 + | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
1.1005 +(*| get_basStr t =
1.1006 + raise error("get_basStr: called with t= "^(term2str t));*)
1.1007 +
1.1008 +(* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1.1009 +fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1.1010 + | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1.1011 + | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1.1012 + | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
1.1013 +(*| get_potStr t =
1.1014 + raise error("get_potStr: called with t= "^(term2str t));*)
1.1015 +
1.1016 +(* Umgekehrte string_ord *)
1.1017 +val string_ord_rev = rev_order o string_ord;
1.1018 +
1.1019 + (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
1.1020 + innerhalb eines Monomes:
1.1021 + - zuerst lexikographisch nach Variablenname
1.1022 + - wenn gleich: nach steigender Potenz *)
1.1023 +fun var_ord (a,b: term) = prod_ord string_ord string_ord
1.1024 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1.1025 +
1.1026 +(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
1.1027 + verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
1.1028 + - zuerst lexikographisch nach Variablenname
1.1029 + - wenn gleich: nach sinkender Potenz*)
1.1030 +fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
1.1031 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1.1032 +
1.1033 +
1.1034 +(* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
1.1035 +val sort_varList = sort var_ord;
1.1036 +
1.1037 +(* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
1.1038 + Argumente in eine Liste *)
1.1039 +fun args u : term list =
1.1040 + let fun stripc (f$t, ts) = stripc (f, t::ts)
1.1041 + | stripc (t as Free _, ts) = (t::ts)
1.1042 + | stripc (_, ts) = ts
1.1043 + in stripc (u, []) end;
1.1044 +
1.1045 +(* liefert True, falls der Term (Liste von Termen) nur Zahlen
1.1046 + (keine Variablen) enthaelt *)
1.1047 +fun filter_num [] = true
1.1048 + | filter_num [Free x] = if (is_num (Free x)) then true
1.1049 + else false
1.1050 + | filter_num ((Free _)::_) = false
1.1051 + | filter_num ts =
1.1052 + (filter_num o (filter_out is_num) o flat o (map args)) ts;
1.1053 +
1.1054 +(* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
1.1055 + dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
1.1056 +fun is_nums t = filter_num [t];
1.1057 +
1.1058 +(* Berechnet den Gesamtgrad eines Monoms *)
1.1059 +local
1.1060 + fun counter (n, []) = n
1.1061 + | counter (n, x :: xs) =
1.1062 + if (is_nums x) then
1.1063 + counter (n, xs)
1.1064 + else
1.1065 + (case x of
1.1066 + (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
1.1067 + if (is_nums (Free (str_h, T))) then
1.1068 + counter (n + (the (int_of_str str_h)), xs)
1.1069 + else counter (n + 1000, xs) (*FIXME.MG?!*)
1.1070 + | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
1.1071 + counter (n + 1000, xs) (*FIXME.MG?!*)
1.1072 + | (Free (str, _)) => counter (n + 1, xs)
1.1073 + (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*)
1.1074 + | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
1.1075 +in
1.1076 + fun monom_degree l = counter (0, l)
1.1077 +end;
1.1078 +
1.1079 +(* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
1.1080 + der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
1.1081 + werden jedoch dabei ignoriert (uebersprungen) *)
1.1082 +fun dict_cond_ord _ _ ([], []) = EQUAL
1.1083 + | dict_cond_ord _ _ ([], _ :: _) = LESS
1.1084 + | dict_cond_ord _ _ (_ :: _, []) = GREATER
1.1085 + | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1.1086 + (case (cond x, cond y) of
1.1087 + (false, false) => (case elem_ord (x, y) of
1.1088 + EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1.1089 + | ord => ord)
1.1090 + | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1.1091 + | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1.1092 + | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
1.1093 +
1.1094 +(* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
1.1095 + zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
1.1096 + dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
1.1097 +fun degree_ord (xs, ys) =
1.1098 + prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
1.1099 + ((monom_degree xs, xs), (monom_degree ys, ys));
1.1100 +
1.1101 +fun hd_str str = substring (str, 0, 1);
1.1102 +fun tl_str str = substring (str, 1, (size str) - 1);
1.1103 +
1.1104 +(* liefert nummerischen Koeffizienten eines Monoms oder None *)
1.1105 +fun get_koeff_of_mon [] = raise error("get_koeff_of_mon: called with l = []")
1.1106 + | get_koeff_of_mon (l as x::xs) = if is_nums x then Some x
1.1107 + else None;
1.1108 +
1.1109 +(* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
1.1110 +fun koeff2ordStr (Some x) = (case x of
1.1111 + (Free (str, T)) =>
1.1112 + if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
1.1113 + else str
1.1114 + | _ => "aaa") (* "num.Ausdruck" --> gross *)
1.1115 + | koeff2ordStr None = "---"; (* "kein Koeff" --> kleinste *)
1.1116 +
1.1117 +(* Order zum Vergleich von Koeffizienten (strings):
1.1118 + "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
1.1119 +fun compare_koeff_ord (xs, ys) =
1.1120 + string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
1.1121 + (koeff2ordStr o get_koeff_of_mon) ys);
1.1122 +
1.1123 +(* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
1.1124 +fun koeff_degree_ord (xs, ys) =
1.1125 + prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
1.1126 +
1.1127 +(* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
1.1128 + Gesamtgradordnung *)
1.1129 +val sort_monList = sort koeff_degree_ord;
1.1130 +
1.1131 +(* Alternativ zu degree_ord koennte auch die viel einfachere und
1.1132 + kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
1.1133 + fuer unsere Zwecke geeignet!
1.1134 +
1.1135 +fun simple_ord (al,bl: term list) = dict_ord string_ord
1.1136 + (map get_basStr al, map get_basStr bl);
1.1137 +
1.1138 +val sort_monList = sort simple_ord; *)
1.1139 +
1.1140 +(* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1.1141 + (mit gewuenschtem Typen T) *)
1.1142 +fun plus T = Const ("op +", [T,T] ---> T);
1.1143 +fun mult T = Const ("op *", [T,T] ---> T);
1.1144 +fun binop op_ t1 t2 = op_ $ t1 $ t2;
1.1145 +fun create_prod T (a,b) = binop (mult T) a b;
1.1146 +fun create_sum T (a,b) = binop (plus T) a b;
1.1147 +
1.1148 +(* löscht letztes Element einer Liste *)
1.1149 +fun drop_last l = take ((length l)-1,l);
1.1150 +
1.1151 +(* Liste von Variablen --> Monom *)
1.1152 +fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
1.1153 +(* Bemerkung:
1.1154 + foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
1.1155 + gleiche Monome zusammengefasst werden können (collect_numerals)!
1.1156 + zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
1.1157 +
1.1158 +(* Liste von Monomen --> Polynom *)
1.1159 +fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
1.1160 +(* Bemerkung:
1.1161 + foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
1.1162 + bessere Darstellung, da keine Klammern sichtbar!
1.1163 + (und discard_parentheses in make_polynomial hat weniger zu tun) *)
1.1164 +
1.1165 +(* sorts the variables (faktors) of an expanded polynomial lexicographical *)
1.1166 +fun sort_variables t =
1.1167 + let
1.1168 + val ll = map monom2list (poly2list t);
1.1169 + val lls = map sort_varList ll;
1.1170 + val T = type_of t;
1.1171 + val ls = map (create_monom T) lls;
1.1172 + in create_polynom T ls end;
1.1173 +
1.1174 +(* sorts the monoms of an expanded and variable-sorted polynomial
1.1175 + by total_degree *)
1.1176 +fun sort_monoms t =
1.1177 + let
1.1178 + val ll = map monom2list (poly2list t);
1.1179 + val lls = sort_monList ll;
1.1180 + val T = type_of t;
1.1181 + val ls = map (create_monom T) lls;
1.1182 + in create_polynom T ls end;
1.1183 +
1.1184 +(* auch Klammerung muss übereinstimmen;
1.1185 + sort_variables klammert Produkte rechtslastig*)
1.1186 +fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
1.1187 +
1.1188 +fun eval_is_multUnordered (thmid:string) _
1.1189 + (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
1.1190 + if is_multUnordered arg
1.1191 + then Some (mk_thmid thmid ""
1.1192 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1193 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1194 + else Some (mk_thmid thmid ""
1.1195 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1196 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.1197 + | eval_is_multUnordered _ _ _ _ = None;
1.1198 +
1.1199 +
1.1200 +fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1.1201 + []:(rule * (term * term list)) list;
1.1202 +fun init_state (_:term) = e_rrlsstate;
1.1203 +fun locate_rule (_:rule list list) (_:term) (_:rule) =
1.1204 + ([]:(rule * (term * term list)) list);
1.1205 +fun next_rule (_:rule list list) (_:term) = (None:rule option);
1.1206 +fun normal_form t = Some (sort_variables t,[]:term list);
1.1207 +
1.1208 +val order_mult_ =
1.1209 + Rrls {id = "order_mult_",
1.1210 + prepat =
1.1211 + [([(term_of o the o (parse thy)) "p is_multUnordered"],
1.1212 + (term_of o the o (parse thy)) "?p" )],
1.1213 + rew_ord = ("dummy_ord", dummy_ord),
1.1214 + erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
1.1215 + [Calc ("Poly.is'_multUnordered", eval_is_multUnordered "")
1.1216 + ],
1.1217 + calc = [("plus" ,("op +" ,eval_binop "#add_")),
1.1218 + ("times" ,("op *" ,eval_binop "#mult_")),
1.1219 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.1220 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.1221 + (*asm_thm=[],*)
1.1222 + scr=Rfuns {init_state = init_state,
1.1223 + normal_form = normal_form,
1.1224 + locate_rule = locate_rule,
1.1225 + next_rule = next_rule,
1.1226 + attach_form = attach_form}};
1.1227 +
1.1228 +val order_mult_rls_ =
1.1229 + Rls{id = "order_mult_rls_", preconds = [],
1.1230 + rew_ord = ("dummy_ord", dummy_ord),
1.1231 + erls = e_rls,srls = Erls,
1.1232 + calc = [],
1.1233 + (*asm_thm = [],*)
1.1234 + rules = [Rls_ order_mult_
1.1235 + ], scr = EmptyScr}:rls;
1.1236 +
1.1237 +fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
1.1238 +
1.1239 +(*WN.18.6.03 *)
1.1240 +(*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
1.1241 +fun eval_is_addUnordered (thmid:string) _
1.1242 + (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
1.1243 + if is_addUnordered arg
1.1244 + then Some (mk_thmid thmid ""
1.1245 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1246 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1247 + else Some (mk_thmid thmid ""
1.1248 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1249 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.1250 + | eval_is_addUnordered _ _ _ _ = None;
1.1251 +
1.1252 +fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1.1253 + []:(rule * (term * term list)) list;
1.1254 +fun init_state (_:term) = e_rrlsstate;
1.1255 +fun locate_rule (_:rule list list) (_:term) (_:rule) =
1.1256 + ([]:(rule * (term * term list)) list);
1.1257 +fun next_rule (_:rule list list) (_:term) = (None:rule option);
1.1258 +fun normal_form t = Some (sort_monoms t,[]:term list);
1.1259 +
1.1260 +val order_add_ =
1.1261 + Rrls {id = "order_add_",
1.1262 + prepat = (*WN.18.6.03 Preconditions und Pattern,
1.1263 + die beide passen muessen, damit das Rrls angewandt wird*)
1.1264 + [([(term_of o the o (parse thy)) "p is_addUnordered"],
1.1265 + (term_of o the o (parse thy)) "?p"
1.1266 + (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1.1267 + fuer die Evaluation der Precondition "p is_addUnordered"*))],
1.1268 + rew_ord = ("dummy_ord", dummy_ord),
1.1269 + erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
1.1270 + [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
1.1271 + (*WN.18.6.03 definiert in Poly.thy,
1.1272 + evaluiert prepat*)],
1.1273 + calc = [("plus" ,("op +" ,eval_binop "#add_")),
1.1274 + ("times" ,("op *" ,eval_binop "#mult_")),
1.1275 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.1276 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.1277 + (*asm_thm=[],*)
1.1278 + scr=Rfuns {init_state = init_state,
1.1279 + normal_form = normal_form,
1.1280 + locate_rule = locate_rule,
1.1281 + next_rule = next_rule,
1.1282 + attach_form = attach_form}};
1.1283 +
1.1284 +val order_add_rls_ =
1.1285 + Rls{id = "order_add_rls_", preconds = [],
1.1286 + rew_ord = ("dummy_ord", dummy_ord),
1.1287 + erls = e_rls,srls = Erls,
1.1288 + calc = [],
1.1289 + (*asm_thm = [],*)
1.1290 + rules = [Rls_ order_add_
1.1291 + ], scr = EmptyScr}:rls;
1.1292 +
1.1293 +(*. see MG-DA.p.52ff .*)
1.1294 +val make_polynomial(*MG.03, overwrites version from above,
1.1295 + previously 'make_polynomial_'*) =
1.1296 + Seq {id = "make_polynomial", preconds = []:term list,
1.1297 + rew_ord = ("dummy_ord", dummy_ord),
1.1298 + erls = Atools_erls, srls = Erls,calc = [],
1.1299 + rules = [Rls_ discard_minus_,
1.1300 + Rls_ expand_poly_,
1.1301 + Calc ("op *", eval_binop "#mult_"),
1.1302 + Rls_ order_mult_rls_,
1.1303 + Rls_ simplify_power_,
1.1304 + Rls_ calc_add_mult_pow_,
1.1305 + Rls_ reduce_012_mult_,
1.1306 + Rls_ order_add_rls_,
1.1307 + Rls_ collect_numerals_,
1.1308 + Rls_ reduce_012_,
1.1309 + Rls_ discard_parentheses_
1.1310 + ],
1.1311 + scr = EmptyScr
1.1312 + }:rls;
1.1313 +val norm_Poly(*=make_polynomial*) =
1.1314 + Seq {id = "norm_Poly", preconds = []:term list,
1.1315 + rew_ord = ("dummy_ord", dummy_ord),
1.1316 + erls = Atools_erls, srls = Erls, calc = [],
1.1317 + rules = [Rls_ discard_minus_,
1.1318 + Rls_ expand_poly_,
1.1319 + Calc ("op *", eval_binop "#mult_"),
1.1320 + Rls_ order_mult_rls_,
1.1321 + Rls_ simplify_power_,
1.1322 + Rls_ calc_add_mult_pow_,
1.1323 + Rls_ reduce_012_mult_,
1.1324 + Rls_ order_add_rls_,
1.1325 + Rls_ collect_numerals_,
1.1326 + Rls_ reduce_012_,
1.1327 + Rls_ discard_parentheses_
1.1328 + ],
1.1329 + scr = EmptyScr
1.1330 + }:rls;
1.1331 +
1.1332 +(* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses_
1.1333 + and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1.1334 +(* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1.1335 +val make_rat_poly_with_parentheses =
1.1336 + Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1.1337 + rew_ord = ("dummy_ord", dummy_ord),
1.1338 + erls = Atools_erls, srls = Erls, calc = [],
1.1339 + rules = [Rls_ discard_minus_,
1.1340 + Rls_ expand_poly_rat_,(*ignors rationals*)
1.1341 + Calc ("op *", eval_binop "#mult_"),
1.1342 + Rls_ order_mult_rls_,
1.1343 + Rls_ simplify_power_,
1.1344 + Rls_ calc_add_mult_pow_,
1.1345 + Rls_ reduce_012_mult_,
1.1346 + Rls_ order_add_rls_,
1.1347 + Rls_ collect_numerals_,
1.1348 + Rls_ reduce_012_
1.1349 + (*Rls_ discard_parentheses_ *)
1.1350 + ],
1.1351 + scr = EmptyScr
1.1352 + }:rls;
1.1353 +
1.1354 +(*.a minimal ruleset for reverse rewriting of factions [2];
1.1355 + compare expand_binoms.*)
1.1356 +val rev_rew_p =
1.1357 +Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1.1358 + erls = Atools_erls, srls = Erls,
1.1359 + calc = [(*("plus" , ("op +", eval_binop "#add_")),
1.1360 + ("times" , ("op *", eval_binop "#mult_")),
1.1361 + ("power_", ("Atools.pow", eval_binop "#power_"))*)
1.1362 + ],
1.1363 + rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.1364 + (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.1365 + Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1),
1.1366 + (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1.1367 + Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
1.1368 + (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1.1369 +
1.1370 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.1371 +
1.1372 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.1373 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.1374 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.1375 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.1376 +
1.1377 + Thm ("real_mult_assoc", num_str real_mult_assoc),
1.1378 + (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1.1379 + Rls_ order_mult_rls_,
1.1380 + (*Rls_ order_add_rls_,*)
1.1381 +
1.1382 + Calc ("op +", eval_binop "#add_"),
1.1383 + Calc ("op *", eval_binop "#mult_"),
1.1384 + Calc ("Atools.pow", eval_binop "#power_"),
1.1385 +
1.1386 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.1387 + (*"r1 * r1 = r1 ^^^ 2"*)
1.1388 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.1389 + (*"z1 + z1 = 2 * z1"*)
1.1390 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.1391 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.1392 +
1.1393 + Thm ("real_num_collect",num_str real_num_collect),
1.1394 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.1395 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.1396 + (*"[| l is_const; m is_const |] ==>
1.1397 + l * n + (m * n + k) = (l + m) * n + k"*)
1.1398 + Thm ("real_one_collect",num_str real_one_collect),
1.1399 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.1400 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.1401 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.1402 +
1.1403 + Thm ("realpow_multI", num_str realpow_multI),
1.1404 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.1405 +
1.1406 + Calc ("op +", eval_binop "#add_"),
1.1407 + Calc ("op *", eval_binop "#mult_"),
1.1408 + Calc ("Atools.pow", eval_binop "#power_"),
1.1409 +
1.1410 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.1411 + Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*)
1.1412 + Thm ("real_add_zero_left",num_str real_add_zero_left)(*0 + z = z*)
1.1413 +
1.1414 + (*Rls_ order_add_rls_*)
1.1415 + ],
1.1416 +
1.1417 + scr = EmptyScr}:rls;
1.1418 +
1.1419 +ruleset' :=
1.1420 +overwritelthy thy (!ruleset',
1.1421 + [("norm_Poly", prep_rls norm_Poly),
1.1422 + ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
1.1423 + ("expand", prep_rls expand),
1.1424 + ("expand_poly", prep_rls expand_poly),
1.1425 + ("simplify_power", prep_rls simplify_power),
1.1426 + ("order_add_mult", prep_rls order_add_mult),
1.1427 + ("collect_numerals", prep_rls collect_numerals),
1.1428 + ("collect_numerals_", prep_rls collect_numerals_),
1.1429 + ("reduce_012", prep_rls reduce_012),
1.1430 + ("discard_parentheses", prep_rls discard_parentheses),
1.1431 + ("make_polynomial", prep_rls make_polynomial),
1.1432 + ("expand_binoms", prep_rls expand_binoms),
1.1433 + ("rev_rew_p", prep_rls rev_rew_p),
1.1434 + ("discard_minus_", prep_rls discard_minus_),
1.1435 + ("expand_poly_", prep_rls expand_poly_),
1.1436 + ("expand_poly_rat_", prep_rls expand_poly_rat_),
1.1437 + ("simplify_power_", prep_rls simplify_power_),
1.1438 + ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
1.1439 + ("reduce_012_mult_", prep_rls reduce_012_mult_),
1.1440 + ("reduce_012_", prep_rls reduce_012_),
1.1441 + ("discard_parentheses_",prep_rls discard_parentheses_),
1.1442 + ("order_mult_rls_", prep_rls order_mult_rls_),
1.1443 + ("order_add_rls_", prep_rls order_add_rls_),
1.1444 + ("make_rat_poly_with_parentheses",
1.1445 + prep_rls make_rat_poly_with_parentheses)
1.1446 + (*("", prep_rls ),
1.1447 + ("", prep_rls ),
1.1448 + ("", prep_rls )
1.1449 + *)
1.1450 + ]);
1.1451 +
1.1452 +calclist':= overwritel (!calclist',
1.1453 + [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1.1454 + eval_is_polyrat_in "#eval_is_polyrat_in")),
1.1455 + ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1.1456 + ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1.1457 + ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1.1458 + ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1.1459 + ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1.1460 + ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
1.1461 + ]);
1.1462 +
1.1463 +
1.1464 +(** problems **)
1.1465 +
1.1466 +store_pbt
1.1467 + (prep_pbt Poly.thy "pbl_simp_poly" [] e_pblID
1.1468 + (["polynomial","simplification"],
1.1469 + [("#Given" ,["term t_"]),
1.1470 + ("#Where" ,["t_ is_polyexp"]),
1.1471 + ("#Find" ,["normalform n_"])
1.1472 + ],
1.1473 + append_rls "e_rls" e_rls [(*for preds in where_*)
1.1474 + Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.1475 + Some "Simplify t_",
1.1476 + [["simplification","for_polynomials"]]));
1.1477 +
1.1478 +
1.1479 +(** methods **)
1.1480 +
1.1481 +store_met
1.1482 + (prep_met Poly.thy "met_simp_poly" [] e_metID
1.1483 + (["simplification","for_polynomials"],
1.1484 + [("#Given" ,["term t_"]),
1.1485 + ("#Where" ,["t_ is_polyexp"]),
1.1486 + ("#Find" ,["normalform n_"])
1.1487 + ],
1.1488 + {rew_ord'="tless_true",
1.1489 + rls' = e_rls,
1.1490 + calc = [],
1.1491 + srls = e_rls,
1.1492 + prls = append_rls "simplification_for_polynomials_prls" e_rls
1.1493 + [(*for preds in where_*)
1.1494 + Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1.1495 + crls = e_rls, nrls = norm_Poly},
1.1496 + "Script SimplifyScript (t_::real) = \
1.1497 + \ ((Rewrite_Set norm_Poly False) t_)"
1.1498 + ));