1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Thu Dec 27 17:44:23 2007 +0100
1.3 @@ -0,0 +1,1484 @@
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_pow2",num_str real_plus_binom_pow2),
1.411 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.412 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.413 + (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.414 + Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
1.415 + (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.416 + Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
1.417 + (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.418 +
1.419 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.420 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.421 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.422 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.423 +
1.424 + Thm ("realpow_multI", num_str realpow_multI),
1.425 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.426 + Thm ("realpow_pow",num_str realpow_pow)
1.427 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.428 + ], scr = EmptyScr}:rls;
1.429 +
1.430 +(*.the expression contains + - * ^ only ?
1.431 + this is weaker than 'is_polynomial' !.*)
1.432 +fun is_polyexp (Free _) = true
1.433 + | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
1.434 + | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
1.435 + | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
1.436 + | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.437 + | is_polyexp (Const ("op +",_) $ t1 $ t2) =
1.438 + ((is_polyexp t1) andalso (is_polyexp t2))
1.439 + | is_polyexp (Const ("op -",_) $ t1 $ t2) =
1.440 + ((is_polyexp t1) andalso (is_polyexp t2))
1.441 + | is_polyexp (Const ("op *",_) $ t1 $ t2) =
1.442 + ((is_polyexp t1) andalso (is_polyexp t2))
1.443 + | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
1.444 + ((is_polyexp t1) andalso (is_polyexp t2))
1.445 + | is_polyexp _ = false;
1.446 +
1.447 +(*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
1.448 +fun eval_is_polyexp (thmid:string) _
1.449 + (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
1.450 + if is_polyexp arg
1.451 + then Some (mk_thmid thmid ""
1.452 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.453 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.454 + else Some (mk_thmid thmid ""
1.455 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.456 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.457 + | eval_is_polyexp _ _ _ _ = None;
1.458 +
1.459 +val expand_poly_rat_ =
1.460 + Rls{id = "expand_poly_rat_", preconds = [],
1.461 + rew_ord = ("dummy_ord", dummy_ord),
1.462 + erls = append_rls "e_rls-is_polyexp" e_rls
1.463 + [Calc ("Poly.is'_polyexp", eval_is_polyexp "")
1.464 + ],
1.465 + srls = Erls,
1.466 + calc = [],
1.467 + (*asm_thm = [],*)
1.468 + rules = [Thm ("real_plus_binom_pow4_poly",num_str real_plus_binom_pow4_poly),
1.469 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
1.470 + Thm ("real_plus_binom_pow5_poly",num_str real_plus_binom_pow5_poly),
1.471 + (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
1.472 + Thm ("real_plus_binom_pow2_poly",num_str real_plus_binom_pow2_poly),
1.473 + (*"[| a is_polyexp; b is_polyexp |] ==>
1.474 + (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.475 + Thm ("real_plus_binom_pow3_poly",num_str real_plus_binom_pow3_poly),
1.476 + (*"[| a is_polyexp; b is_polyexp |] ==>
1.477 + (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.478 + Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
1.479 + (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.480 + Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
1.481 + (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.482 +
1.483 + Thm ("real_add_mult_distrib_poly" ,num_str real_add_mult_distrib_poly),
1.484 + (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.485 + Thm ("real_add_mult_distrib2_poly",num_str real_add_mult_distrib2_poly),
1.486 + (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.487 +
1.488 + Thm ("realpow_multI_poly", num_str realpow_multI_poly),
1.489 + (*"[| r is_polyexp; s is_polyexp |] ==>
1.490 + (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.491 + Thm ("realpow_pow",num_str realpow_pow)
1.492 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.493 + ], scr = EmptyScr}:rls;
1.494 +
1.495 +val simplify_power_ =
1.496 + Rls{id = "simplify_power_", preconds = [],
1.497 + rew_ord = ("dummy_ord", dummy_ord),
1.498 + erls = e_rls, srls = Erls,
1.499 + calc = [],
1.500 + (*asm_thm = [],*)
1.501 + rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.502 + a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
1.503 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.504 + (*"r * r = r ^^^ 2"*)
1.505 + Thm ("realpow_twoI_assoc_l",num_str realpow_twoI_assoc_l),
1.506 + (*"r * (r * s) = r ^^^ 2 * s"*)
1.507 +
1.508 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.509 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.510 + Thm ("realpow_plus_1_assoc_l", num_str realpow_plus_1_assoc_l),
1.511 + (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
1.512 + (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
1.513 + Thm ("realpow_plus_1_assoc_l2", num_str realpow_plus_1_assoc_l2),
1.514 + (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
1.515 +
1.516 + Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.517 + (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.518 + Thm ("realpow_addI_assoc_l", num_str realpow_addI_assoc_l),
1.519 + (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
1.520 +
1.521 + (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
1.522 + "r * r = r ^^^ 2" wenn r=a^^^b*)
1.523 + Thm ("realpow_pow",num_str realpow_pow)
1.524 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.525 + ], scr = EmptyScr}:rls;
1.526 +
1.527 +val calc_add_mult_pow_ =
1.528 + Rls{id = "calc_add_mult_pow_", preconds = [],
1.529 + rew_ord = ("dummy_ord", dummy_ord),
1.530 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.531 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.532 + ("times" , ("op *", eval_binop "#mult_")),
1.533 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.534 + ],
1.535 + (*asm_thm = [],*)
1.536 + rules = [Calc ("op +", eval_binop "#add_"),
1.537 + Calc ("op *", eval_binop "#mult_"),
1.538 + Calc ("Atools.pow", eval_binop "#power_")
1.539 + ], scr = EmptyScr}:rls;
1.540 +
1.541 +val reduce_012_mult_ =
1.542 + Rls{id = "reduce_012_mult_", preconds = [],
1.543 + rew_ord = ("dummy_ord", dummy_ord),
1.544 + erls = e_rls,srls = Erls,
1.545 + calc = [],
1.546 + (*asm_thm = [],*)
1.547 + rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
1.548 + Thm ("real_mult_1_right",num_str real_mult_1_right),
1.549 + (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
1.550 + Thm ("realpow_zeroI",num_str realpow_zeroI),
1.551 + (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
1.552 + Thm ("realpow_oneI",num_str realpow_oneI),
1.553 + (*"r ^^^ 1 = r"*)
1.554 + Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.555 + (*"1 ^^^ n = 1"*)
1.556 + ], scr = EmptyScr}:rls;
1.557 +
1.558 +val collect_numerals_ =
1.559 + Rls{id = "collect_numerals_", preconds = [],
1.560 + rew_ord = ("dummy_ord", dummy_ord),
1.561 + erls = Atools_erls, srls = Erls,
1.562 + calc = [("plus" , ("op +", eval_binop "#add_"))
1.563 + ],
1.564 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.565 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.566 + Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
1.567 + (*"[| l is_const; m is_const |] ==> \
1.568 + \(k + m * n) + l * n = k + (l + m)*n"*)
1.569 + Thm ("real_one_collect",num_str real_one_collect),
1.570 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.571 + Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
1.572 + (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.573 +
1.574 + Calc ("op +", eval_binop "#add_"),
1.575 +
1.576 + (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.577 + (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.578 + Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
1.579 + (*"(k + z1) + z1 = k + 2 * z1"*)
1.580 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
1.581 + (*"z1 + z1 = 2 * z1"*)
1.582 +
1.583 + ], scr = EmptyScr}:rls;
1.584 +
1.585 +val reduce_012_ =
1.586 + Rls{id = "reduce_012_", preconds = [],
1.587 + rew_ord = ("dummy_ord", dummy_ord),
1.588 + erls = e_rls,srls = Erls,
1.589 + calc = [],
1.590 + (*asm_thm = [],*)
1.591 + rules = [Thm ("real_mult_1",num_str real_mult_1),
1.592 + (*"1 * z = z"*)
1.593 + Thm ("real_mult_0",num_str real_mult_0),
1.594 + (*"0 * z = 0"*)
1.595 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.596 + (*"0 + z = z"*)
1.597 + Thm ("real_add_zero_right",num_str real_add_zero_right),
1.598 + (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
1.599 +
1.600 + (*Thm ("realpow_oneI",num_str realpow_oneI)*)
1.601 + (*"?r ^^^ 1 = ?r"*)
1.602 + Thm ("real_0_divide",num_str real_0_divide)(*WN060914*)
1.603 + (*"0 / ?x = 0"*)
1.604 + ], scr = EmptyScr}:rls;
1.605 +
1.606 +(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.607 +val discard_parentheses_ =
1.608 + append_rls "discard_parentheses_" e_rls
1.609 + [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
1.610 + (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
1.611 + (*Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))*)
1.612 + (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
1.613 + ];
1.614 +
1.615 +(*----------------- End: rulesets for make_polynomial_ -----------------*)
1.616 +
1.617 +(*MG.0401 ev. for use in rls with ordered rewriting ?
1.618 +val collect_numerals_left =
1.619 + Rls{id = "collect_numerals", preconds = [],
1.620 + rew_ord = ("dummy_ord", dummy_ord),
1.621 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.622 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.623 + ("times" , ("op *", eval_binop "#mult_")),
1.624 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.625 + ],
1.626 + (*asm_thm = [],*)
1.627 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.628 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.629 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.630 + (*"[| l is_const; m is_const |] ==>
1.631 + l * n + (m * n + k) = (l + m) * n + k"*)
1.632 + Thm ("real_one_collect",num_str real_one_collect),
1.633 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.634 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.635 + (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
1.636 +
1.637 + Calc ("op +", eval_binop "#add_"),
1.638 +
1.639 + (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
1.640 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.641 + (*"z1 + z1 = 2 * z1"*)
1.642 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.643 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.644 + ], scr = EmptyScr}:rls;*)
1.645 +
1.646 +val expand_poly =
1.647 + Rls{id = "expand_poly", preconds = [],
1.648 + rew_ord = ("dummy_ord", dummy_ord),
1.649 + erls = e_rls,srls = Erls,
1.650 + calc = [],
1.651 + (*asm_thm = [],*)
1.652 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.653 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.654 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.655 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.656 + (*Thm ("real_add_mult_distrib1",num_str real_add_mult_distrib1),
1.657 + ....... 18.3.03 undefined???*)
1.658 +
1.659 + Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.660 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.661 + Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p),
1.662 + (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
1.663 + Thm ("real_plus_minus_binom1_p",
1.664 + num_str real_plus_minus_binom1_p),
1.665 + (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
1.666 + Thm ("real_plus_minus_binom2_p",
1.667 + num_str real_plus_minus_binom2_p),
1.668 + (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.669 +
1.670 + Thm ("real_minus_minus",num_str real_minus_minus),
1.671 + (*"- (- ?z) = ?z"*)
1.672 + Thm ("real_diff_minus",num_str real_diff_minus),
1.673 + (*"a - b = a + -1 * b"*)
1.674 + Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.675 + (*- ?z = "-1 * ?z"*)
1.676 +
1.677 + (*Thm ("",num_str ),
1.678 + Thm ("",num_str ),
1.679 + Thm ("",num_str ),*)
1.680 + (*Thm ("real_minus_add_distrib",
1.681 + num_str real_minus_add_distrib),*)
1.682 + (*"- (?x + ?y) = - ?x + - ?y"*)
1.683 + (*Thm ("real_diff_plus",num_str real_diff_plus)*)
1.684 + (*"a - b = a + -b"*)
1.685 + ], scr = EmptyScr}:rls;
1.686 +val simplify_power =
1.687 + Rls{id = "simplify_power", preconds = [],
1.688 + rew_ord = ("dummy_ord", dummy_ord),
1.689 + erls = e_rls, srls = Erls,
1.690 + calc = [],
1.691 + (*asm_thm = [],*)
1.692 + rules = [Thm ("realpow_multI", num_str realpow_multI),
1.693 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.694 +
1.695 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.696 + (*"r1 * r1 = r1 ^^^ 2"*)
1.697 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.698 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.699 + Thm ("realpow_pow",num_str realpow_pow),
1.700 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.701 + Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.702 + (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.703 + Thm ("realpow_oneI",num_str realpow_oneI),
1.704 + (*"r ^^^ 1 = r"*)
1.705 + Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.706 + (*"1 ^^^ n = 1"*)
1.707 + ], scr = EmptyScr}:rls;
1.708 +(*MG.0401: termorders for multivariate polys dropped due to principal problems:
1.709 + (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1.710 +val order_add_mult =
1.711 + Rls{id = "order_add_mult", preconds = [],
1.712 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.713 + erls = e_rls,srls = Erls,
1.714 + calc = [],
1.715 + (*asm_thm = [],*)
1.716 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.717 + (* z * w = w * z *)
1.718 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.719 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.720 + Thm ("real_mult_assoc",num_str real_mult_assoc),
1.721 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.722 + Thm ("real_add_commute",num_str real_add_commute),
1.723 + (*z + w = w + z*)
1.724 + Thm ("real_add_left_commute",num_str real_add_left_commute),
1.725 + (*x + (y + z) = y + (x + z)*)
1.726 + Thm ("real_add_assoc",num_str real_add_assoc)
1.727 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.728 + ], scr = EmptyScr}:rls;
1.729 +(*MG.0401: termorders for multivariate polys dropped due to principal problems:
1.730 + (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1.731 +val order_mult =
1.732 + Rls{id = "order_mult", preconds = [],
1.733 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.734 + erls = e_rls,srls = Erls,
1.735 + calc = [],
1.736 + (*asm_thm = [],*)
1.737 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.738 + (* z * w = w * z *)
1.739 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.740 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.741 + Thm ("real_mult_assoc",num_str real_mult_assoc)
1.742 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.743 + ], scr = EmptyScr}:rls;
1.744 +val collect_numerals =
1.745 + Rls{id = "collect_numerals", preconds = [],
1.746 + rew_ord = ("dummy_ord", dummy_ord),
1.747 + erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.748 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.749 + ("times" , ("op *", eval_binop "#mult_")),
1.750 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.751 + ],
1.752 + (*asm_thm = [],*)
1.753 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.754 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.755 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.756 + (*"[| l is_const; m is_const |] ==>
1.757 + l * n + (m * n + k) = (l + m) * n + k"*)
1.758 + Thm ("real_one_collect",num_str real_one_collect),
1.759 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.760 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.761 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.762 + Calc ("op +", eval_binop "#add_"),
1.763 + Calc ("op *", eval_binop "#mult_"),
1.764 + Calc ("Atools.pow", eval_binop "#power_")
1.765 + ], scr = EmptyScr}:rls;
1.766 +val reduce_012 =
1.767 + Rls{id = "reduce_012", preconds = [],
1.768 + rew_ord = ("dummy_ord", dummy_ord),
1.769 + erls = e_rls,srls = Erls,
1.770 + calc = [],
1.771 + (*asm_thm = [],*)
1.772 + rules = [Thm ("real_mult_1",num_str real_mult_1),
1.773 + (*"1 * z = z"*)
1.774 + (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
1.775 + (*"-1 * z = - z"*)
1.776 + Thm ("sym_real_mult_minus_eq1",
1.777 + num_str (real_mult_minus_eq1 RS sym)),
1.778 + (*- (?x * ?y) = "- ?x * ?y"*)
1.779 + (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
1.780 + (*"- ?x * - ?y = ?x * ?y"*)---*)
1.781 + Thm ("real_mult_0",num_str real_mult_0),
1.782 + (*"0 * z = 0"*)
1.783 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.784 + (*"0 + z = z"*)
1.785 + Thm ("real_add_minus",num_str real_add_minus),
1.786 + (*"?z + - ?z = 0"*)
1.787 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.788 + (*"z1 + z1 = 2 * z1"*)
1.789 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.790 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.791 + ], scr = EmptyScr}:rls;
1.792 +(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.793 +val discard_parentheses =
1.794 + append_rls "discard_parentheses" e_rls
1.795 + [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)),
1.796 + Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))];
1.797 +
1.798 +val scr_make_polynomial =
1.799 +"Script Expand_binoms t_ =\
1.800 +\(Repeat \
1.801 +\((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.802 +
1.803 +\ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \
1.804 +\ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \
1.805 +\ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \
1.806 +\ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \
1.807 +
1.808 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.809 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.810 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.811 +
1.812 +\ (Try (Repeat (Rewrite real_mult_commute False))) @@ \
1.813 +\ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \
1.814 +\ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \
1.815 +\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.816 +\ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \
1.817 +\ (Try (Repeat (Rewrite real_add_assoc False))) @@ \
1.818 +
1.819 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.820 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.821 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.822 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.823 +
1.824 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.825 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.826 +
1.827 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.828 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.829 +
1.830 +\ (Try (Repeat (Calculate plus ))) @@ \
1.831 +\ (Try (Repeat (Calculate times ))) @@ \
1.832 +\ (Try (Repeat (Calculate power_)))) \
1.833 +\ t_)";
1.834 +
1.835 +(*version used by MG.02/03, overwritten by version AG in 04 below
1.836 +val make_polynomial = prep_rls(
1.837 + Seq{id = "make_polynomial", preconds = []:term list,
1.838 + rew_ord = ("dummy_ord", dummy_ord),
1.839 + erls = Atools_erls, srls = Erls,
1.840 + calc = [],(*asm_thm = [],*)
1.841 + rules = [Rls_ expand_poly,
1.842 + Rls_ order_add_mult,
1.843 + Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
1.844 + Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
1.845 + Rls_ reduce_012,
1.846 + Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
1.847 + Rls_ discard_parentheses
1.848 + ],
1.849 + scr = EmptyScr
1.850 + }:rls); *)
1.851 +
1.852 +val scr_expand_binoms =
1.853 +"Script Expand_binoms t_ =\
1.854 +\(Repeat \
1.855 +\((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \
1.856 +\ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \
1.857 +\ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \
1.858 +\ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \
1.859 +\ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \
1.860 +\ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \
1.861 +
1.862 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.863 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.864 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.865 +
1.866 +\ (Try (Repeat (Calculate plus ))) @@ \
1.867 +\ (Try (Repeat (Calculate times ))) @@ \
1.868 +\ (Try (Repeat (Calculate power_))) @@ \
1.869 +
1.870 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.871 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.872 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.873 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.874 +
1.875 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.876 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.877 +
1.878 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.879 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.880 +
1.881 +\ (Try (Repeat (Calculate plus ))) @@ \
1.882 +\ (Try (Repeat (Calculate times ))) @@ \
1.883 +\ (Try (Repeat (Calculate power_)))) \
1.884 +\ t_)";
1.885 +
1.886 +val expand_binoms =
1.887 + Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.888 + erls = Atools_erls, srls = Erls,
1.889 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.890 + ("times" , ("op *", eval_binop "#mult_")),
1.891 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.892 + ],
1.893 + (*asm_thm = [],*)
1.894 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.895 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.896 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.897 + (*"(a + b)*(a + b) = ...*)
1.898 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.899 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.900 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.901 + (*"(a - b)*(a - b) = ...*)
1.902 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.903 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.904 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.905 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.906 + (*RL 020915*)
1.907 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.908 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.909 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.910 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.911 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.912 + (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1.913 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.914 + (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1.915 + Thm ("realpow_multI",num_str realpow_multI),
1.916 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.917 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.918 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.919 + Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.920 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.921 +
1.922 +
1.923 + (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.924 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.925 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.926 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.927 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.928 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.929 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.930 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.931 + *)
1.932 +
1.933 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
1.934 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
1.935 + Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
1.936 +
1.937 + Calc ("op +", eval_binop "#add_"),
1.938 + Calc ("op *", eval_binop "#mult_"),
1.939 + Calc ("Atools.pow", eval_binop "#power_"),
1.940 + (*
1.941 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.942 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.943 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.944 + Thm ("real_add_commute",num_str real_add_commute), (**)
1.945 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
1.946 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
1.947 + *)
1.948 +
1.949 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.950 + (*"r1 * r1 = r1 ^^^ 2"*)
1.951 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.952 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.953 + (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.954 + (*"z1 + z1 = 2 * z1"*)*)
1.955 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.956 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.957 +
1.958 + Thm ("real_num_collect",num_str real_num_collect),
1.959 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.960 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.961 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.962 + Thm ("real_one_collect",num_str real_one_collect),
1.963 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.964 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.965 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.966 +
1.967 + Calc ("op +", eval_binop "#add_"),
1.968 + Calc ("op *", eval_binop "#mult_"),
1.969 + Calc ("Atools.pow", eval_binop "#power_")
1.970 + ],
1.971 + scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
1.972 + }:rls;
1.973 +
1.974 +
1.975 +"******* Poly.ML end ******* ...RL";
1.976 +
1.977 +
1.978 +(**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
1.979 +
1.980 +(*FIXME.0401: make SML-order local to make_polynomial(_) *)
1.981 +(*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1.982 +(* Polynom --> List von Monomen *)
1.983 +fun poly2list (Const ("op +",_) $ t1 $ t2) =
1.984 + (poly2list t1) @ (poly2list t2)
1.985 + | poly2list t = [t];
1.986 +
1.987 +(* Monom --> Liste von Variablen *)
1.988 +fun monom2list (Const ("op *",_) $ t1 $ t2) =
1.989 + (monom2list t1) @ (monom2list t2)
1.990 + | monom2list t = [t];
1.991 +
1.992 +(* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1.993 +fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1.994 + | get_basStr (Free (str, _)) = str
1.995 + | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
1.996 +(*| get_basStr t =
1.997 + raise error("get_basStr: called with t= "^(term2str t));*)
1.998 +
1.999 +(* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1.1000 +fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1.1001 + | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1.1002 + | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1.1003 + | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
1.1004 +(*| get_potStr t =
1.1005 + raise error("get_potStr: called with t= "^(term2str t));*)
1.1006 +
1.1007 +(* Umgekehrte string_ord *)
1.1008 +val string_ord_rev = rev_order o string_ord;
1.1009 +
1.1010 + (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
1.1011 + innerhalb eines Monomes:
1.1012 + - zuerst lexikographisch nach Variablenname
1.1013 + - wenn gleich: nach steigender Potenz *)
1.1014 +fun var_ord (a,b: term) = prod_ord string_ord string_ord
1.1015 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1.1016 +
1.1017 +(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
1.1018 + verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
1.1019 + - zuerst lexikographisch nach Variablenname
1.1020 + - wenn gleich: nach sinkender Potenz*)
1.1021 +fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
1.1022 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1.1023 +
1.1024 +
1.1025 +(* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
1.1026 +val sort_varList = sort var_ord;
1.1027 +
1.1028 +(* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
1.1029 + Argumente in eine Liste *)
1.1030 +fun args u : term list =
1.1031 + let fun stripc (f$t, ts) = stripc (f, t::ts)
1.1032 + | stripc (t as Free _, ts) = (t::ts)
1.1033 + | stripc (_, ts) = ts
1.1034 + in stripc (u, []) end;
1.1035 +
1.1036 +(* liefert True, falls der Term (Liste von Termen) nur Zahlen
1.1037 + (keine Variablen) enthaelt *)
1.1038 +fun filter_num [] = true
1.1039 + | filter_num [Free x] = if (is_num (Free x)) then true
1.1040 + else false
1.1041 + | filter_num ((Free _)::_) = false
1.1042 + | filter_num ts =
1.1043 + (filter_num o (filter_out is_num) o flat o (map args)) ts;
1.1044 +
1.1045 +(* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
1.1046 + dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
1.1047 +fun is_nums t = filter_num [t];
1.1048 +
1.1049 +(* Berechnet den Gesamtgrad eines Monoms *)
1.1050 +local
1.1051 + fun counter (n, []) = n
1.1052 + | counter (n, x :: xs) =
1.1053 + if (is_nums x) then
1.1054 + counter (n, xs)
1.1055 + else
1.1056 + (case x of
1.1057 + (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
1.1058 + if (is_nums (Free (str_h, T))) then
1.1059 + counter (n + (the (int_of_str str_h)), xs)
1.1060 + else counter (n + 1000, xs) (*FIXME.MG?!*)
1.1061 + | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
1.1062 + counter (n + 1000, xs) (*FIXME.MG?!*)
1.1063 + | (Free (str, _)) => counter (n + 1, xs)
1.1064 + (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*)
1.1065 + | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
1.1066 +in
1.1067 + fun monom_degree l = counter (0, l)
1.1068 +end;
1.1069 +
1.1070 +(* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
1.1071 + der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
1.1072 + werden jedoch dabei ignoriert (uebersprungen) *)
1.1073 +fun dict_cond_ord _ _ ([], []) = EQUAL
1.1074 + | dict_cond_ord _ _ ([], _ :: _) = LESS
1.1075 + | dict_cond_ord _ _ (_ :: _, []) = GREATER
1.1076 + | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1.1077 + (case (cond x, cond y) of
1.1078 + (false, false) => (case elem_ord (x, y) of
1.1079 + EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1.1080 + | ord => ord)
1.1081 + | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1.1082 + | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1.1083 + | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
1.1084 +
1.1085 +(* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
1.1086 + zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
1.1087 + dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
1.1088 +fun degree_ord (xs, ys) =
1.1089 + prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
1.1090 + ((monom_degree xs, xs), (monom_degree ys, ys));
1.1091 +
1.1092 +fun hd_str str = substring (str, 0, 1);
1.1093 +fun tl_str str = substring (str, 1, (size str) - 1);
1.1094 +
1.1095 +(* liefert nummerischen Koeffizienten eines Monoms oder None *)
1.1096 +fun get_koeff_of_mon [] = raise error("get_koeff_of_mon: called with l = []")
1.1097 + | get_koeff_of_mon (l as x::xs) = if is_nums x then Some x
1.1098 + else None;
1.1099 +
1.1100 +(* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
1.1101 +fun koeff2ordStr (Some x) = (case x of
1.1102 + (Free (str, T)) =>
1.1103 + if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
1.1104 + else str
1.1105 + | _ => "aaa") (* "num.Ausdruck" --> gross *)
1.1106 + | koeff2ordStr None = "---"; (* "kein Koeff" --> kleinste *)
1.1107 +
1.1108 +(* Order zum Vergleich von Koeffizienten (strings):
1.1109 + "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
1.1110 +fun compare_koeff_ord (xs, ys) =
1.1111 + string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
1.1112 + (koeff2ordStr o get_koeff_of_mon) ys);
1.1113 +
1.1114 +(* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
1.1115 +fun koeff_degree_ord (xs, ys) =
1.1116 + prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
1.1117 +
1.1118 +(* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
1.1119 + Gesamtgradordnung *)
1.1120 +val sort_monList = sort koeff_degree_ord;
1.1121 +
1.1122 +(* Alternativ zu degree_ord koennte auch die viel einfachere und
1.1123 + kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
1.1124 + fuer unsere Zwecke geeignet!
1.1125 +
1.1126 +fun simple_ord (al,bl: term list) = dict_ord string_ord
1.1127 + (map get_basStr al, map get_basStr bl);
1.1128 +
1.1129 +val sort_monList = sort simple_ord; *)
1.1130 +
1.1131 +(* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1.1132 + (mit gewuenschtem Typen T) *)
1.1133 +fun plus T = Const ("op +", [T,T] ---> T);
1.1134 +fun mult T = Const ("op *", [T,T] ---> T);
1.1135 +fun binop op_ t1 t2 = op_ $ t1 $ t2;
1.1136 +fun create_prod T (a,b) = binop (mult T) a b;
1.1137 +fun create_sum T (a,b) = binop (plus T) a b;
1.1138 +
1.1139 +(* löscht letztes Element einer Liste *)
1.1140 +fun drop_last l = take ((length l)-1,l);
1.1141 +
1.1142 +(* Liste von Variablen --> Monom *)
1.1143 +fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
1.1144 +(* Bemerkung:
1.1145 + foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
1.1146 + gleiche Monome zusammengefasst werden können (collect_numerals)!
1.1147 + zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
1.1148 +
1.1149 +(* Liste von Monomen --> Polynom *)
1.1150 +fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
1.1151 +(* Bemerkung:
1.1152 + foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
1.1153 + bessere Darstellung, da keine Klammern sichtbar!
1.1154 + (und discard_parentheses in make_polynomial hat weniger zu tun) *)
1.1155 +
1.1156 +(* sorts the variables (faktors) of an expanded polynomial lexicographical *)
1.1157 +fun sort_variables t =
1.1158 + let
1.1159 + val ll = map monom2list (poly2list t);
1.1160 + val lls = map sort_varList ll;
1.1161 + val T = type_of t;
1.1162 + val ls = map (create_monom T) lls;
1.1163 + in create_polynom T ls end;
1.1164 +
1.1165 +(* sorts the monoms of an expanded and variable-sorted polynomial
1.1166 + by total_degree *)
1.1167 +fun sort_monoms t =
1.1168 + let
1.1169 + val ll = map monom2list (poly2list t);
1.1170 + val lls = sort_monList ll;
1.1171 + val T = type_of t;
1.1172 + val ls = map (create_monom T) lls;
1.1173 + in create_polynom T ls end;
1.1174 +
1.1175 +(* auch Klammerung muss übereinstimmen;
1.1176 + sort_variables klammert Produkte rechtslastig*)
1.1177 +fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
1.1178 +
1.1179 +fun eval_is_multUnordered (thmid:string) _
1.1180 + (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
1.1181 + if is_multUnordered arg
1.1182 + then Some (mk_thmid thmid ""
1.1183 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1184 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1185 + else Some (mk_thmid thmid ""
1.1186 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1187 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.1188 + | eval_is_multUnordered _ _ _ _ = None;
1.1189 +
1.1190 +
1.1191 +fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1.1192 + []:(rule * (term * term list)) list;
1.1193 +fun init_state (_:term) = e_rrlsstate;
1.1194 +fun locate_rule (_:rule list list) (_:term) (_:rule) =
1.1195 + ([]:(rule * (term * term list)) list);
1.1196 +fun next_rule (_:rule list list) (_:term) = (None:rule option);
1.1197 +fun normal_form t = Some (sort_variables t,[]:term list);
1.1198 +
1.1199 +val order_mult_ =
1.1200 + Rrls {id = "order_mult_",
1.1201 + prepat =
1.1202 + [([(term_of o the o (parse thy)) "p is_multUnordered"],
1.1203 + (term_of o the o (parse thy)) "?p" )],
1.1204 + rew_ord = ("dummy_ord", dummy_ord),
1.1205 + erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
1.1206 + [Calc ("Poly.is'_multUnordered", eval_is_multUnordered "")
1.1207 + ],
1.1208 + calc = [("plus" ,("op +" ,eval_binop "#add_")),
1.1209 + ("times" ,("op *" ,eval_binop "#mult_")),
1.1210 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.1211 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.1212 + (*asm_thm=[],*)
1.1213 + scr=Rfuns {init_state = init_state,
1.1214 + normal_form = normal_form,
1.1215 + locate_rule = locate_rule,
1.1216 + next_rule = next_rule,
1.1217 + attach_form = attach_form}};
1.1218 +
1.1219 +val order_mult_rls_ =
1.1220 + Rls{id = "order_mult_rls_", preconds = [],
1.1221 + rew_ord = ("dummy_ord", dummy_ord),
1.1222 + erls = e_rls,srls = Erls,
1.1223 + calc = [],
1.1224 + (*asm_thm = [],*)
1.1225 + rules = [Rls_ order_mult_
1.1226 + ], scr = EmptyScr}:rls;
1.1227 +
1.1228 +fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
1.1229 +
1.1230 +(*WN.18.6.03 *)
1.1231 +(*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
1.1232 +fun eval_is_addUnordered (thmid:string) _
1.1233 + (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
1.1234 + if is_addUnordered arg
1.1235 + then Some (mk_thmid thmid ""
1.1236 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1237 + Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1238 + else Some (mk_thmid thmid ""
1.1239 + ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
1.1240 + Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.1241 + | eval_is_addUnordered _ _ _ _ = None;
1.1242 +
1.1243 +fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1.1244 + []:(rule * (term * term list)) list;
1.1245 +fun init_state (_:term) = e_rrlsstate;
1.1246 +fun locate_rule (_:rule list list) (_:term) (_:rule) =
1.1247 + ([]:(rule * (term * term list)) list);
1.1248 +fun next_rule (_:rule list list) (_:term) = (None:rule option);
1.1249 +fun normal_form t = Some (sort_monoms t,[]:term list);
1.1250 +
1.1251 +val order_add_ =
1.1252 + Rrls {id = "order_add_",
1.1253 + prepat = (*WN.18.6.03 Preconditions und Pattern,
1.1254 + die beide passen muessen, damit das Rrls angewandt wird*)
1.1255 + [([(term_of o the o (parse thy)) "p is_addUnordered"],
1.1256 + (term_of o the o (parse thy)) "?p"
1.1257 + (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1.1258 + fuer die Evaluation der Precondition "p is_addUnordered"*))],
1.1259 + rew_ord = ("dummy_ord", dummy_ord),
1.1260 + erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
1.1261 + [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
1.1262 + (*WN.18.6.03 definiert in Poly.thy,
1.1263 + evaluiert prepat*)],
1.1264 + calc = [("plus" ,("op +" ,eval_binop "#add_")),
1.1265 + ("times" ,("op *" ,eval_binop "#mult_")),
1.1266 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.1267 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.1268 + (*asm_thm=[],*)
1.1269 + scr=Rfuns {init_state = init_state,
1.1270 + normal_form = normal_form,
1.1271 + locate_rule = locate_rule,
1.1272 + next_rule = next_rule,
1.1273 + attach_form = attach_form}};
1.1274 +
1.1275 +val order_add_rls_ =
1.1276 + Rls{id = "order_add_rls_", preconds = [],
1.1277 + rew_ord = ("dummy_ord", dummy_ord),
1.1278 + erls = e_rls,srls = Erls,
1.1279 + calc = [],
1.1280 + (*asm_thm = [],*)
1.1281 + rules = [Rls_ order_add_
1.1282 + ], scr = EmptyScr}:rls;
1.1283 +
1.1284 +(*. see MG-DA.p.52ff .*)
1.1285 +val make_polynomial(*MG.03, overwrites version from above,
1.1286 + previously 'make_polynomial_'*) =
1.1287 + Seq {id = "make_polynomial", preconds = []:term list,
1.1288 + rew_ord = ("dummy_ord", dummy_ord),
1.1289 + erls = Atools_erls, srls = Erls,calc = [],
1.1290 + rules = [Rls_ discard_minus_,
1.1291 + Rls_ expand_poly_,
1.1292 + Calc ("op *", eval_binop "#mult_"),
1.1293 + Rls_ order_mult_rls_,
1.1294 + Rls_ simplify_power_,
1.1295 + Rls_ calc_add_mult_pow_,
1.1296 + Rls_ reduce_012_mult_,
1.1297 + Rls_ order_add_rls_,
1.1298 + Rls_ collect_numerals_,
1.1299 + Rls_ reduce_012_,
1.1300 + Rls_ discard_parentheses_
1.1301 + ],
1.1302 + scr = EmptyScr
1.1303 + }:rls;
1.1304 +val norm_Poly(*=make_polynomial*) =
1.1305 + Seq {id = "norm_Poly", preconds = []:term list,
1.1306 + rew_ord = ("dummy_ord", dummy_ord),
1.1307 + erls = Atools_erls, srls = Erls, calc = [],
1.1308 + rules = [Rls_ discard_minus_,
1.1309 + Rls_ expand_poly_,
1.1310 + Calc ("op *", eval_binop "#mult_"),
1.1311 + Rls_ order_mult_rls_,
1.1312 + Rls_ simplify_power_,
1.1313 + Rls_ calc_add_mult_pow_,
1.1314 + Rls_ reduce_012_mult_,
1.1315 + Rls_ order_add_rls_,
1.1316 + Rls_ collect_numerals_,
1.1317 + Rls_ reduce_012_,
1.1318 + Rls_ discard_parentheses_
1.1319 + ],
1.1320 + scr = EmptyScr
1.1321 + }:rls;
1.1322 +
1.1323 +(* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses_
1.1324 + and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1.1325 +(* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1.1326 +val make_rat_poly_with_parentheses =
1.1327 + Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1.1328 + rew_ord = ("dummy_ord", dummy_ord),
1.1329 + erls = Atools_erls, srls = Erls, calc = [],
1.1330 + rules = [Rls_ discard_minus_,
1.1331 + Rls_ expand_poly_rat_,(*ignors rationals*)
1.1332 + Calc ("op *", eval_binop "#mult_"),
1.1333 + Rls_ order_mult_rls_,
1.1334 + Rls_ simplify_power_,
1.1335 + Rls_ calc_add_mult_pow_,
1.1336 + Rls_ reduce_012_mult_,
1.1337 + Rls_ order_add_rls_,
1.1338 + Rls_ collect_numerals_,
1.1339 + Rls_ reduce_012_
1.1340 + (*Rls_ discard_parentheses_ *)
1.1341 + ],
1.1342 + scr = EmptyScr
1.1343 + }:rls;
1.1344 +
1.1345 +(*.a minimal ruleset for reverse rewriting of factions [2];
1.1346 + compare expand_binoms.*)
1.1347 +val rev_rew_p =
1.1348 +Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1.1349 + erls = Atools_erls, srls = Erls,
1.1350 + calc = [(*("plus" , ("op +", eval_binop "#add_")),
1.1351 + ("times" , ("op *", eval_binop "#mult_")),
1.1352 + ("power_", ("Atools.pow", eval_binop "#power_"))*)
1.1353 + ],
1.1354 + rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.1355 + (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.1356 + Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1),
1.1357 + (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1.1358 + Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
1.1359 + (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1.1360 +
1.1361 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.1362 +
1.1363 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.1364 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.1365 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.1366 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.1367 +
1.1368 + Thm ("real_mult_assoc", num_str real_mult_assoc),
1.1369 + (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1.1370 + Rls_ order_mult_rls_,
1.1371 + (*Rls_ order_add_rls_,*)
1.1372 +
1.1373 + Calc ("op +", eval_binop "#add_"),
1.1374 + Calc ("op *", eval_binop "#mult_"),
1.1375 + Calc ("Atools.pow", eval_binop "#power_"),
1.1376 +
1.1377 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.1378 + (*"r1 * r1 = r1 ^^^ 2"*)
1.1379 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.1380 + (*"z1 + z1 = 2 * z1"*)
1.1381 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.1382 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.1383 +
1.1384 + Thm ("real_num_collect",num_str real_num_collect),
1.1385 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.1386 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.1387 + (*"[| l is_const; m is_const |] ==>
1.1388 + l * n + (m * n + k) = (l + m) * n + k"*)
1.1389 + Thm ("real_one_collect",num_str real_one_collect),
1.1390 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.1391 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.1392 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.1393 +
1.1394 + Thm ("realpow_multI", num_str realpow_multI),
1.1395 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.1396 +
1.1397 + Calc ("op +", eval_binop "#add_"),
1.1398 + Calc ("op *", eval_binop "#mult_"),
1.1399 + Calc ("Atools.pow", eval_binop "#power_"),
1.1400 +
1.1401 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.1402 + Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*)
1.1403 + Thm ("real_add_zero_left",num_str real_add_zero_left)(*0 + z = z*)
1.1404 +
1.1405 + (*Rls_ order_add_rls_*)
1.1406 + ],
1.1407 +
1.1408 + scr = EmptyScr}:rls;
1.1409 +
1.1410 +ruleset' :=
1.1411 +overwritelthy thy (!ruleset',
1.1412 + [("norm_Poly", prep_rls norm_Poly),
1.1413 + ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
1.1414 + ("expand", prep_rls expand),
1.1415 + ("expand_poly", prep_rls expand_poly),
1.1416 + ("simplify_power", prep_rls simplify_power),
1.1417 + ("order_add_mult", prep_rls order_add_mult),
1.1418 + ("collect_numerals", prep_rls collect_numerals),
1.1419 + ("collect_numerals_", prep_rls collect_numerals_),
1.1420 + ("reduce_012", prep_rls reduce_012),
1.1421 + ("discard_parentheses", prep_rls discard_parentheses),
1.1422 + ("make_polynomial", prep_rls make_polynomial),
1.1423 + ("expand_binoms", prep_rls expand_binoms),
1.1424 + ("rev_rew_p", prep_rls rev_rew_p),
1.1425 + ("discard_minus_", prep_rls discard_minus_),
1.1426 + ("expand_poly_", prep_rls expand_poly_),
1.1427 + ("expand_poly_rat_", prep_rls expand_poly_rat_),
1.1428 + ("simplify_power_", prep_rls simplify_power_),
1.1429 + ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
1.1430 + ("reduce_012_mult_", prep_rls reduce_012_mult_),
1.1431 + ("reduce_012_", prep_rls reduce_012_),
1.1432 + ("discard_parentheses_",prep_rls discard_parentheses_),
1.1433 + ("order_mult_rls_", prep_rls order_mult_rls_),
1.1434 + ("order_add_rls_", prep_rls order_add_rls_),
1.1435 + ("make_rat_poly_with_parentheses",
1.1436 + prep_rls make_rat_poly_with_parentheses)
1.1437 + (*("", prep_rls ),
1.1438 + ("", prep_rls ),
1.1439 + ("", prep_rls )
1.1440 + *)
1.1441 + ]);
1.1442 +
1.1443 +calclist':= overwritel (!calclist',
1.1444 + [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1.1445 + eval_is_polyrat_in "#eval_is_polyrat_in")),
1.1446 + ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1.1447 + ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1.1448 + ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1.1449 + ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1.1450 + ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1.1451 + ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
1.1452 + ]);
1.1453 +
1.1454 +(** problems **)
1.1455 +
1.1456 +store_pbt
1.1457 + (prep_pbt Poly.thy "pbl_simp_poly" [] e_pblID
1.1458 + (["polynomial","simplification"],
1.1459 + [("#Given" ,["term t_"]),
1.1460 + ("#Where" ,["t_ is_polyexp"]),
1.1461 + ("#Find" ,["normalform n_"])
1.1462 + ],
1.1463 + append_rls "e_rls" e_rls [(*for preds in where_*)
1.1464 + Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.1465 + Some "Simplify t_",
1.1466 + [["simplification","for_polynomials"]]));
1.1467 +
1.1468 +(** methods **)
1.1469 +
1.1470 +store_met
1.1471 + (prep_met Poly.thy "met_simp_poly" [] e_metID
1.1472 + (["simplification","for_polynomials"],
1.1473 + [("#Given" ,["term t_"]),
1.1474 + ("#Where" ,["t_ is_polyexp"]),
1.1475 + ("#Find" ,["normalform n_"])
1.1476 + ],
1.1477 + {rew_ord'="tless_true",
1.1478 + rls' = e_rls,
1.1479 + calc = [],
1.1480 + srls = e_rls,
1.1481 + prls = append_rls "simplification_for_polynomials_prls" e_rls
1.1482 + [(*for preds in where_*)
1.1483 + Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1.1484 + crls = e_rls, nrls = norm_Poly},
1.1485 + "Script SimplifyScript (t_::real) = \
1.1486 + \ ((Rewrite_Set norm_Poly False) t_)"
1.1487 + ));
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Thu Dec 27 15:20:44 2007 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Thu Dec 27 17:44:23 2007 +0100
2.3 @@ -24,7 +24,6 @@
2.4 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
2.5 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
2.6 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
2.7 - (writeln ("@@@ eval_kleiner: " ^ term2str p);
2.8 if is_num a andalso is_num b then
2.9 if int_of_Free a < int_of_Free b then
2.10 Some ((term2str p) ^ " = True",
2.11 @@ -33,13 +32,28 @@
2.12 Trueprop $ (mk_equality (p, HOLogic.false_const)))
2.13 else
2.14 if identifier a < identifier b then
2.15 - (writeln ("@@@ eval_kleiner: " ^ term2str p ^ " = True");
2.16 Some ((term2str p) ^ " = True",
2.17 Trueprop $ (mk_equality (p, HOLogic.true_const)))
2.18 - )
2.19 else Some ((term2str p) ^ " = False",
2.20 Trueprop $ (mk_equality (p, HOLogic.false_const)))
2.21 - )
2.22 + | eval_kleiner _ _ _ _ = None;
2.23 +fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
2.24 + if is_num b then
2.25 + if is_num a then
2.26 + if int_of_Free a < int_of_Free b then
2.27 + Some ((term2str p) ^ " = True",
2.28 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
2.29 + else Some ((term2str p) ^ " = False",
2.30 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
2.31 + else (* -1 * -2 kleiner 0 *)
2.32 + Some ((term2str p) ^ " = False",
2.33 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
2.34 + else
2.35 + if identifier a < identifier b then
2.36 + Some ((term2str p) ^ " = True",
2.37 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
2.38 + else Some ((term2str p) ^ " = False",
2.39 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
2.40 | eval_kleiner _ _ _ _ = None;
2.41
2.42 fun ist_monom (Free (id,_)) = true
2.43 @@ -58,7 +72,6 @@
2.44 | eval_ist_monom _ _ _ _ = None;
2.45
2.46
2.47 -
2.48 (** rewrite order **)
2.49
2.50 (** rulesets **)
2.51 @@ -87,6 +100,64 @@
2.52 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
2.53 ], scr = EmptyScr}:rls;
2.54
2.55 +val fasse_zusammen =
2.56 + Rls{id = "fasse_zusammen", preconds = [],
2.57 + rew_ord = ("dummy_ord", dummy_ord),
2.58 + erls = append_rls "erls_fasse_zusammen" e_rls
2.59 + [Calc ("Atools.is'_const",eval_const "#is_const_")],
2.60 + srls = Erls, calc = [],
2.61 + rules =
2.62 + [Thm ("real_num_collect",num_str real_num_collect),
2.63 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
2.64 + Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
2.65 + (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
2.66 + Thm ("real_one_collect",num_str real_one_collect),
2.67 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
2.68 + Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
2.69 + (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
2.70 +
2.71 + Thm ("addiere_x_plus_minus",num_str addiere_x_plus_minus),
2.72 + (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
2.73 + Thm ("addiere_x_minus_plus",num_str addiere_x_minus_plus),
2.74 + (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
2.75 + Thm ("addiere_x_minus_minus",num_str addiere_x_minus_minus),
2.76 + (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
2.77 +
2.78 + Calc ("op +", eval_binop "#add_"),
2.79 + Calc ("op -", eval_binop "#subtr_"),
2.80 +
2.81 + (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
2.82 + (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
2.83 + Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
2.84 + (*"(k + z1) + z1 = k + 2 * z1"*)
2.85 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
2.86 + (*"z1 + z1 = 2 * z1"*)
2.87 +
2.88 + ], scr = EmptyScr}:rls;
2.89 +
2.90 +val verschoenere =
2.91 + Rls{id = "verschoenere", preconds = [],
2.92 + rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
2.93 + erls = append_rls "erls_verschoenere" e_rls
2.94 + [Calc ("PolyMinus.kleiner", eval_kleiner "")],
2.95 + rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
2.96 + (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
2.97 + Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
2.98 + (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
2.99 + Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
2.100 + (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
2.101 + Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
2.102 + (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
2.103 + Calc ("op *", eval_binop "#mult_")
2.104 + ], scr = EmptyScr}:rls;
2.105 +
2.106 +ruleset' :=
2.107 +overwritelthy thy (!ruleset',
2.108 + [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
2.109 + ("fasse_zusammen", prep_rls fasse_zusammen),
2.110 + ("verschoenere", prep_rls verschoenere)
2.111 + ]);
2.112 +
2.113 (** problems **)
2.114
2.115 (** methods **)
3.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Thu Dec 27 15:20:44 2007 +0100
3.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Thu Dec 27 17:44:23 2007 +0100
3.3 @@ -22,5 +22,17 @@
3.4 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
3.5 tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
3.6
3.7 + addiere_x_plus_minus "[| l is_const; m is_const |] ==> \
3.8 + \(k + m * n) - l * n = k + (m - l) * n"
3.9 + addiere_x_minus_plus "[| l is_const; m is_const |] ==> \
3.10 + \(k - m * n) + l * n = k + (-m + l) * n"
3.11 + addiere_x_minus_minus "[| l is_const; m is_const |] ==> \
3.12 + \(k - m * n) - l * n = k + (-m - l) * n"
3.13 +
3.14 + vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
3.15 + vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
3.16 + vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
3.17 + vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
3.18 +
3.19 end
3.20
4.1 --- a/src/sml/Scripts/rewrite.sml Thu Dec 27 15:20:44 2007 +0100
4.2 +++ b/src/sml/Scripts/rewrite.sml Thu Dec 27 17:44:23 2007 +0100
4.3 @@ -151,7 +151,8 @@
4.4 writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
4.5 val ct = app_num_tr'2 ct
4.6 in case get_calculation_ thy cc ct of
4.7 - None => rew_once ruls asm ct apno thms
4.8 + None => ((*writeln "@@@ rewrite__set_: get_calculation_-> None";*)
4.9 + rew_once ruls asm ct apno thms)
4.10 | Some (thmid, thm') =>
4.11 let
4.12 val pairopt =
5.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Thu Dec 27 15:20:44 2007 +0100
5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Thu Dec 27 17:44:23 2007 +0100
5.3 @@ -6,13 +6,15 @@
5.4 use"../smltest/IsacKnowledge/polyminus.sml";
5.5 use"polyminus.sml";
5.6 *)
5.7 -val thy = EqSystem.thy;
5.8 +val thy = PolyMinus.thy;
5.9
5.10 "-----------------------------------------------------------------";
5.11 "table of contents -----------------------------------------------";
5.12 "-----------------------------------------------------------------";
5.13 "----------- watch order_add_mult -------------------------------";
5.14 "----------- build predicate for +- ordering ---------------------";
5.15 +"----------- build fasse_zuswammen -------------------------------";
5.16 +"----------- build verschoenere ----------------------------------";
5.17 "-----------------------------------------------------------------";
5.18 "-----------------------------------------------------------------";
5.19 "-----------------------------------------------------------------";
5.20 @@ -23,6 +25,7 @@
5.21 "----------- watch order_add_mult -------------------------------";
5.22 "----- with these simple variables it works...";
5.23 trace_rewrite:=true;
5.24 +trace_rewrite:=false;
5.25 val t = str2term "((a + d) + c) + b";
5.26 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
5.27 if term2str t = "a + (b + (c + d))" then ()
5.28 @@ -69,7 +72,6 @@
5.29 (*@@@ rew_sub gosub: t = d + (b + a + c)
5.30 @@@ rew_sub begin: t = b + a + c*)
5.31
5.32 -(*#####################################################################
5.33
5.34 "----------- build predicate for +- ordering ---------------------";
5.35 "----------- build predicate for +- ordering ---------------------";
5.36 @@ -91,16 +93,22 @@
5.37 Some ("a kleiner b = True", _) => ()
5.38 | _ => raise error "polyminus.sml: a kleiner b = True";
5.39
5.40 -"----- test rewrite_, rewrite_set_";
5.41 +"----- compare tausche_plus with real_num_collect";
5.42 val od = dummy_ord;
5.43 +
5.44 val erls = erls_ordne_alphabetisch;
5.45 val t = str2term "b + a";
5.46 -"############################################";
5.47 val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
5.48 if term2str t = "a + b" then ()
5.49 else raise error "polyminus.sml: ordne_alphabetisch1 b + a";
5.50
5.51 +val erls = Atools_erls;
5.52 +val t = str2term "2*a + 3*a";
5.53 +val Some (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t;
5.54 +
5.55 +"----- test rewrite_, rewrite_set_";
5.56 trace_rewrite:=true;
5.57 +val erls = erls_ordne_alphabetisch;
5.58 val t = str2term "b + a";
5.59 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
5.60 if term2str t = "a + b" then ()
5.61 @@ -136,14 +144,31 @@
5.62 "----- compile rls for the most complicated terms";
5.63 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
5.64 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
5.65 -val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
5.66 -"5 * e - 8 * g + 6 * f - 9 - 7 * e + 10 * g - 4 * f + 12";
5.67 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
5.68 +if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
5.69 +then () else raise error "polyminus.sml: ordne_alphabetisch finished";
5.70
5.71
5.72 +"----------- build fasse_zuswammen -------------------------------";
5.73 +"----------- build fasse_zuswammen -------------------------------";
5.74 +"----------- build fasse_zuswammen -------------------------------";
5.75 +val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
5.76 +val Some (t,_) = rewrite_set_ thy false fasse_zusammen t;
5.77 +if term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()
5.78 +else raise error "polyminus.sml: fasse_zusammen finished";
5.79 +
5.80 +"----------- build verschoenere ----------------------------------";
5.81 +"----------- build verschoenere ----------------------------------";
5.82 +"----------- build verschoenere ----------------------------------";
5.83 +val t = str2term "3 + -2 * e + 2 * f + 2 * g";
5.84 +val Some (t,_) = rewrite_set_ thy false verschoenere t;
5.85 +if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
5.86 +else raise error "polyminus.sml: verschoenere 3 + -2 * e ...";
5.87 +
5.88 +trace_rewrite:=true;
5.89 trace_rewrite:=false;
5.90 (*
5.91 use"../smltest/IsacKnowledge/polyminus.sml";
5.92 use"polyminus.sml";
5.93 *)
5.94
5.95 -#####################################################################*)