1.1 --- a/src/Tools/isac/IsacKnowledge/Poly.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1495 +0,0 @@
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 = member op = (vars c) v;
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 (member op = (vars c) v);
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 - ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
1.335 - (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\"");
1.336 - val _=writeln("u= g@us= \""^
1.337 - ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
1.338 - (commas(map(Syntax.string_of_term (thy2ctxt 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 - ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.460 - Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.461 - else SOME (mk_thmid thmid ""
1.462 - ((Syntax.string_of_term (thy2ctxt 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 - ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.1193 - Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1194 - else SOME (mk_thmid thmid ""
1.1195 - ((Syntax.string_of_term (thy2ctxt 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 - ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1.1246 - Trueprop $ (mk_equality (t, HOLogic.true_const)))
1.1247 - else SOME (mk_thmid thmid ""
1.1248 - ((Syntax.string_of_term (thy2ctxt 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 - ));