1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,744 @@
1.4 +(* changed by: rlang
1.5 + last change by: rlang
1.6 + date: 02.11.28
1.7 +*)
1.8 +
1.9 +(*
1.10 + use"../knowledge/Poly.ML";
1.11 + use"knowledge/Poly.ML";
1.12 + use"Poly.ML";
1.13 +
1.14 + remove_thy"Poly";
1.15 + use_thy"knowledge/Isac";
1.16 +
1.17 + use"ROOT.ML";
1.18 + cd"knowledge";
1.19 + *)
1.20 +"******* Poly.ML begin *******";
1.21 +
1.22 +theory' := overwritel (!theory', [("Poly.thy",Poly.thy)]);
1.23 +
1.24 +
1.25 +(* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
1.26 +fun is_polyrat_in t v =
1.27 + let
1.28 + fun coeff_in c v = v mem (vars c);
1.29 + fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
1.30 + (* at the moment there is no term like this, but ....*)
1.31 + | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = not(coeff_in b v)
1.32 + | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) orelse (finddivide t2 v)
1.33 + | finddivide (_ $ t1) v = (finddivide t1 v)
1.34 + | finddivide _ _ = false;
1.35 + in
1.36 + finddivide t v
1.37 + end;
1.38 +
1.39 +fun eval_is_polyrat_in _ _ (p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
1.40 + if is_polyrat_in t v then
1.41 + Some ((term2str p) ^ " = True",
1.42 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.43 + else Some ((term2str p) ^ " = True",
1.44 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.45 + | eval_is_polyrat_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);
1.46 +
1.47 +
1.48 +local
1.49 + (*.a 'c is coefficient of v' if v does NOT occur in c.*)
1.50 + fun coeff_in c v = not (v mem (vars c));
1.51 + (*
1.52 + val v = (term_of o the o (parse thy)) "x";
1.53 + val t = (term_of o the o (parse thy)) "1";
1.54 + coeff_in t v;
1.55 + (*val it = true : bool*)
1.56 + val t = (term_of o the o (parse thy)) "a*b+c";
1.57 + coeff_in t v;
1.58 + (*val it = true : bool*)
1.59 + val t = (term_of o the o (parse thy)) "a*x+c";
1.60 + coeff_in t v;
1.61 + (*val it = false : bool*)
1.62 + *)
1.63 + (*. a 'monomial t in variable v' is a term t with
1.64 + either (1) v NOT existent in t, or (2) v contained in t,
1.65 + if (1) then degree 0
1.66 + if (2) then v is a factor on the very right, ev. with exponent.*)
1.67 + fun factor_right_deg (*case 2*)
1.68 + (t as Const ("op *",_) $ t1 $
1.69 + (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
1.70 + if ((vv = v) andalso (coeff_in t1 v)) then Some (int_of_str' d) else None
1.71 + | factor_right_deg
1.72 + (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
1.73 + if (vv = v) then Some (int_of_str' d) else None
1.74 + | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
1.75 + if ((vv = v) andalso (coeff_in t1 v))then Some 1 else None
1.76 + | factor_right_deg vv v =
1.77 + if (vv = v) then Some 1 else None;
1.78 + fun mono_deg_in m v =
1.79 + if coeff_in m v then (*case 1*) Some 0
1.80 + else factor_right_deg m 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)) "(a*b+c)*x^^^7";
1.84 + mono_deg_in t v;
1.85 + (*val it = Some 7*)
1.86 + val t = (term_of o the o (parse thy)) "x^^^7";
1.87 + mono_deg_in t v;
1.88 + (*val it = Some 7*)
1.89 + val t = (term_of o the o (parse thy)) "(a*b+c)*x";
1.90 + mono_deg_in t v;
1.91 + (*val it = Some 1*)
1.92 + val t = (term_of o the o (parse thy)) "(a*b+x)*x";
1.93 + mono_deg_in t v;
1.94 + (*val it = None*)
1.95 + val t = (term_of o the o (parse thy)) "x";
1.96 + mono_deg_in t v;
1.97 + (*val it = Some 1*)
1.98 + val t = (term_of o the o (parse thy)) "(a*b+c)";
1.99 + mono_deg_in t v;
1.100 + (*val it = Some 0*)
1.101 + val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
1.102 + mono_deg_in t v;
1.103 + (*val it = None*)
1.104 + *)
1.105 + fun expand_deg_in t v =
1.106 + let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.107 + (case mono_deg_in t2 v of (* $ is left associative*)
1.108 + Some d' => edi d' d' t1
1.109 + | None => None)
1.110 + | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
1.111 + (case mono_deg_in t2 v of
1.112 + Some d' => edi d' d' t1
1.113 + | None => None)
1.114 + | edi d dmax (Const ("op -",_) $ t1 $ t2) =
1.115 + (case mono_deg_in t2 v of
1.116 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.117 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.118 + | None => None)
1.119 + | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.120 + (case mono_deg_in t2 v of
1.121 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.122 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.123 + | None => None)
1.124 + | edi ~1 ~1 t =
1.125 + (case mono_deg_in t v of
1.126 + d as Some _ => d
1.127 + | None => None)
1.128 + | edi d dmax t = (*basecase last*)
1.129 + (case mono_deg_in t v of
1.130 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then Some dmax else None
1.131 + | None => None)
1.132 + in edi ~1 ~1 t end;
1.133 + (*
1.134 + val v = (term_of o the o (parse thy)) "x";
1.135 + val t = (term_of o the o (parse thy)) "a+b";
1.136 + expand_deg_in t v;
1.137 + (*val it = Some 0*)
1.138 + val t = (term_of o the o (parse thy)) "(a+b)*x";
1.139 + expand_deg_in t v;
1.140 + (*Some 1*)
1.141 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
1.142 + expand_deg_in t v;
1.143 + (*Some 1*)
1.144 + val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
1.145 + expand_deg_in t v;
1.146 + (*Some 1*)
1.147 + val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
1.148 + expand_deg_in t v;
1.149 + *)
1.150 + fun poly_deg_in t v =
1.151 + let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.152 + (case mono_deg_in t2 v of (* $ is left associative*)
1.153 + Some d' => edi d' d' t1
1.154 + | None => None)
1.155 + | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.156 + (case mono_deg_in t2 v of
1.157 + (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.158 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else None
1.159 + | None => None)
1.160 + | edi ~1 ~1 t =
1.161 + (case mono_deg_in t v of
1.162 + d as Some _ => d
1.163 + | None => None)
1.164 + | edi d dmax t = (*basecase last*)
1.165 + (case mono_deg_in t v of
1.166 + Some d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then Some dmax else None
1.167 + | None => None)
1.168 + in edi ~1 ~1 t end;
1.169 +in
1.170 +
1.171 +fun is_expanded_in t v =
1.172 + case expand_deg_in t v of Some _ => true | None => false;
1.173 +fun is_poly_in t v =
1.174 + case poly_deg_in t v of Some _ => true | None => false;
1.175 +fun has_degree_in t v =
1.176 + case expand_deg_in t v of Some d => d | None => ~1;
1.177 +end;
1.178 +(*
1.179 + val v = (term_of o the o (parse thy)) "x";
1.180 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
1.181 + has_degree_in t v;
1.182 + (*val it = 2*)
1.183 + val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
1.184 + has_degree_in t v;
1.185 + (*val it = 2*)
1.186 + val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
1.187 + has_degree_in t v;
1.188 + (*val it = 2*)
1.189 +*)
1.190 +
1.191 +(*
1.192 + use"../knowledge/Poly.ML";
1.193 + use"knowledge/Poly.ML";
1.194 + use"Poly.ML";
1.195 + *)
1.196 +
1.197 +(*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
1.198 +fun eval_is_expanded_in _ _
1.199 + (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
1.200 + if is_expanded_in t v
1.201 + then Some ((term2str p) ^ " = True",
1.202 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.203 + else Some ((term2str p) ^ " = True",
1.204 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.205 + | eval_is_expanded_in _ _ _ _ = None;
1.206 +(*
1.207 + val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.208 + val Some (id, t') = eval_is_expanded_in 0 0 t 0;
1.209 + (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
1.210 + term2str t';
1.211 + (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
1.212 +*)
1.213 +(*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
1.214 +fun eval_is_poly_in _ _
1.215 + (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
1.216 + if is_poly_in t v
1.217 + then Some ((term2str p) ^ " = True",
1.218 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.219 + else Some ((term2str p) ^ " = True",
1.220 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.221 + | eval_is_poly_in _ _ _ _ = None;
1.222 +(*
1.223 + val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
1.224 + val Some (id, t') = eval_is_poly_in 0 0 t 0;
1.225 + (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
1.226 + term2str t';
1.227 + (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
1.228 +*)
1.229 +
1.230 +(*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
1.231 +fun eval_has_degree_in _ _
1.232 + (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
1.233 + let val d = has_degree_in t v
1.234 + val d' = term_of_num HOLogic.realT d
1.235 + in Some ((term2str p) ^ " = " ^ (string_of_int d),
1.236 + Trueprop $ (mk_equality (p, d')))
1.237 + end
1.238 + | eval_has_degree_in _ _ _ _ = None;
1.239 +(*
1.240 +> val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
1.241 +> val Some (id, t') = eval_has_degree_in 0 0 t 0;
1.242 +val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
1.243 +> term2str t';
1.244 +val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
1.245 +*)
1.246 +
1.247 +(*..*)
1.248 +val calculate_Poly =
1.249 + append_rls "calculate_PolyFIXXXME.not.impl." e_rls
1.250 + [];
1.251 +
1.252 +(*.for evaluation of conditions in rewrite rules.*)
1.253 +val poly_erls =
1.254 + merge_rls "poly_erls" atools_erls
1.255 + (append_rls "ops_preds" e_rls
1.256 + [ Calc ("op =",eval_equal "#equal_"),
1.257 + Thm ("real_unari_minus",num_str real_unari_minus),
1.258 + Calc ("op +",eval_binop "#add_"),
1.259 + Calc ("op -",eval_binop "#subtract_"),
1.260 + Calc ("op *",eval_binop "#mult_"),
1.261 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.262 + Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
1.263 + Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
1.264 + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
1.265 + Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
1.266 + Calc ("Atools.occurs'_in",eval_occurs_in "")
1.267 + ]);
1.268 +ruleset' := overwritel (!ruleset',
1.269 + [("poly_erls",poly_erls)(*FIXXXME:del with rls.rls'*)
1.270 + ]);
1.271 +
1.272 +local (*. for make_polynomial .*)
1.273 +
1.274 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.275 +
1.276 +fun pr_ord EQUAL = "EQUAL"
1.277 + | pr_ord LESS = "LESS"
1.278 + | pr_ord GREATER = "GREATER";
1.279 +
1.280 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.281 + (case a of
1.282 + "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1.283 + | _ => (((a, 0), T), 0))
1.284 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.285 + | dest_hd' (Var v) = (v, 2)
1.286 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.287 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.288 +
1.289 +fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
1.290 + (case int_of_str (order) of
1.291 + Some d => d
1.292 + | None => 0)
1.293 + | get_order_pow _ = 0;
1.294 +
1.295 +fun size_of_term' (Const(str,_) $ t) =
1.296 + if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
1.297 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.298 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.299 + | size_of_term' _ = 1;
1.300 +
1.301 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.302 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.303 + | term_ord' pr thy (t, u) =
1.304 + (if pr then
1.305 + let
1.306 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.307 + val _=writeln("t= f@ts= \""^
1.308 + ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
1.309 + (commas(map(string_of_cterm o cterm_of (sign_of thy))ts))^"]\"");
1.310 + val _=writeln("u= g@us= \""^
1.311 + ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
1.312 + (commas(map(string_of_cterm o cterm_of (sign_of thy))us))^"]\"");
1.313 + val _=writeln("size_of_term(t,u)= ("^
1.314 + (string_of_int(size_of_term' t))^", "^
1.315 + (string_of_int(size_of_term' u))^")");
1.316 + val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
1.317 + val _=writeln("terms_ord(ts,us) = "^
1.318 + ((pr_ord o terms_ord str false)(ts,us)));
1.319 + val _=writeln("-------");
1.320 + in () end
1.321 + else ();
1.322 + case int_ord (size_of_term' t, size_of_term' u) of
1.323 + EQUAL =>
1.324 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.325 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.326 + | ord => ord)
1.327 + end
1.328 + | ord => ord)
1.329 +and hd_ord (f, g) = (* ~ term.ML *)
1.330 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.331 +and terms_ord str pr (ts, us) =
1.332 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.333 +in
1.334 +
1.335 +fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
1.336 + (term_ord' pr thy(***) tu = LESS );
1.337 +
1.338 +end;(*local*)
1.339 +
1.340 +local (*. poly_order for x * y * x^^^2 .*)
1.341 +
1.342 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.343 +
1.344 +fun pr_ord EQUAL = "EQUAL"
1.345 + | pr_ord LESS = "LESS"
1.346 + | pr_ord GREATER = "GREATER";
1.347 +
1.348 +fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.349 + (case a of
1.350 + "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
1.351 + | _ => (((a, 0), T), 0))
1.352 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.353 + | dest_hd' (Var v) = (v, 2)
1.354 + | dest_hd' (Bound i) = ((("", i), dummyT), 3)
1.355 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
1.356 +
1.357 +fun size_of_term' (Const(str,_) $ t) =
1.358 + if "Atools.pow"= str then 1000 + size_of_term' t
1.359 + else 1 + size_of_term' t (*WN*)
1.360 + | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.361 + | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.362 + | size_of_term' _ = 1;
1.363 +
1.364 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.365 + (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1.366 + | term_ord' pr thy (t, u) =
1.367 + (case int_ord (size_of_term' t, size_of_term' u) of
1.368 + EQUAL =>
1.369 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.370 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.371 + | ord => ord)
1.372 + end
1.373 + | ord => ord)
1.374 +and hd_ord (f, g) = (* ~ term.ML *)
1.375 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.376 +and terms_ord str pr (ts, us) =
1.377 + list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.378 +in
1.379 +
1.380 +fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
1.381 + (term_ord' pr thy(***) tu = LESS );
1.382 +
1.383 +end;(*local*)
1.384 +
1.385 +rew_ord' := overwritel (!rew_ord',
1.386 +[("termlessI", termlessI),
1.387 + ("ord_make_polynomial", ord_make_polynomial false thy)
1.388 + ]);
1.389 +
1.390 +
1.391 +val expand =
1.392 + Rls{id = "expand", preconds = [],
1.393 + rew_ord = ("dummy_ord", dummy_ord),
1.394 + erls = e_rls,srls = Erls,
1.395 + calc = [],
1.396 + asm_thm = [],
1.397 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.398 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.399 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2)
1.400 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.401 + ], scr = EmptyScr}:rls;
1.402 +
1.403 +val expand_poly =
1.404 + Rls{id = "expand_poly", preconds = [],
1.405 + rew_ord = ("dummy_ord", dummy_ord),
1.406 + erls = e_rls,srls = Erls,
1.407 + calc = [],
1.408 + asm_thm = [],
1.409 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.410 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.411 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.412 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.413 + (*Thm ("real_add_mult_distrib1",num_str real_add_mult_distrib1),
1.414 + ....... 18.3.03 undefined???*)
1.415 +
1.416 + Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.417 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.418 + Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p),
1.419 + (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
1.420 + Thm ("real_plus_minus_binom1_p",
1.421 + num_str real_plus_minus_binom1_p),
1.422 + (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
1.423 + Thm ("real_plus_minus_binom2_p",
1.424 + num_str real_plus_minus_binom2_p),
1.425 + (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.426 +
1.427 + Thm ("real_minus_minus",num_str real_minus_minus),
1.428 + (*"- (- ?z) = ?z"*)
1.429 + Thm ("real_diff_minus",num_str real_diff_minus),
1.430 + (*"a - b = a + -1 * b"*)
1.431 + Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.432 + (*- ?z = "-1 * ?z"*)
1.433 +
1.434 + (*Thm ("",num_str ),
1.435 + Thm ("",num_str ),
1.436 + Thm ("",num_str ),*)
1.437 + (*Thm ("real_minus_add_distrib",
1.438 + num_str real_minus_add_distrib),*)
1.439 + (*"- (?x + ?y) = - ?x + - ?y"*)
1.440 + (*Thm ("real_diff_plus",num_str real_diff_plus)*)
1.441 + (*"a - b = a + -b"*)
1.442 + ], scr = EmptyScr}:rls;
1.443 +val simplify_power =
1.444 + Rls{id = "simplify_power", preconds = [],
1.445 + rew_ord = ("dummy_ord", dummy_ord),
1.446 + erls = e_rls, srls = Erls,
1.447 + calc = [],
1.448 + asm_thm = [],
1.449 + rules = [Thm ("realpow_multI", num_str realpow_multI),
1.450 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.451 +
1.452 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.453 + (*"r1 * r1 = r1 ^^^ 2"*)
1.454 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.455 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.456 + Thm ("realpow_pow",num_str realpow_pow),
1.457 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.458 + Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.459 + (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.460 + Thm ("realpow_oneI",num_str realpow_oneI),
1.461 + (*"r ^^^ 1 = r"*)
1.462 + Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.463 + (*"1 ^^^ n = 1"*)
1.464 + ], scr = EmptyScr}:rls;
1.465 +val order_add_mult =
1.466 + Rls{id = "order_add_mult", preconds = [],
1.467 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.468 + erls = e_rls,srls = Erls,
1.469 + calc = [],
1.470 + asm_thm = [],
1.471 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.472 + (* z * w = w * z *)
1.473 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.474 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.475 + Thm ("real_mult_assoc",num_str real_mult_assoc),
1.476 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.477 + Thm ("real_add_commute",num_str real_add_commute),
1.478 + (*z + w = w + z*)
1.479 + Thm ("real_add_left_commute",num_str real_add_left_commute),
1.480 + (*x + (y + z) = y + (x + z)*)
1.481 + Thm ("real_add_assoc",num_str real_add_assoc)
1.482 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.483 + ], scr = EmptyScr}:rls;
1.484 +val order_mult =
1.485 + Rls{id = "order_mult", preconds = [],
1.486 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
1.487 + erls = e_rls,srls = Erls,
1.488 + calc = [],
1.489 + asm_thm = [],
1.490 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.491 + (* z * w = w * z *)
1.492 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.493 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.494 + Thm ("real_mult_assoc",num_str real_mult_assoc)
1.495 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.496 + ], scr = EmptyScr}:rls;
1.497 +val collect_numerals =
1.498 + Rls{id = "collect_numerals", preconds = [],
1.499 + rew_ord = ("dummy_ord", dummy_ord),
1.500 + erls = atools_erls(*erls3.4.03*),srls = Erls,
1.501 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.502 + ("times" , ("op *", eval_binop "#mult_")),
1.503 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.504 + ],
1.505 + asm_thm = [],
1.506 + rules = [Thm ("real_num_collect",num_str real_num_collect),
1.507 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.508 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.509 + (*"[| l is_const; m is_const |] ==>
1.510 + l * n + (m * n + k) = (l + m) * n + k"*)
1.511 + Thm ("real_one_collect",num_str real_one_collect),
1.512 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.513 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.514 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.515 + Calc ("op +", eval_binop "#add_"),
1.516 + Calc ("op *", eval_binop "#mult_"),
1.517 + Calc ("Atools.pow", eval_binop "#power_")
1.518 + ], scr = EmptyScr}:rls;
1.519 +val reduce_012 =
1.520 + Rls{id = "reduce_012", preconds = [],
1.521 + rew_ord = ("dummy_ord", dummy_ord),
1.522 + erls = e_rls,srls = Erls,
1.523 + calc = [],
1.524 + asm_thm = [],
1.525 + rules = [Thm ("real_mult_1",num_str real_mult_1),
1.526 + (*"1 * z = z"*)
1.527 + (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
1.528 + (*"-1 * z = - z"*)
1.529 + Thm ("sym_real_mult_minus_eq1",
1.530 + num_str (real_mult_minus_eq1 RS sym)),
1.531 + (*- (?x * ?y) = "- ?x * ?y"*)
1.532 + (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
1.533 + (*"- ?x * - ?y = ?x * ?y"*)---*)
1.534 + Thm ("real_mult_0",num_str real_mult_0),
1.535 + (*"0 * z = 0"*)
1.536 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.537 + (*"0 + z = z"*)
1.538 + Thm ("real_add_minus",num_str real_add_minus),
1.539 + (*"?z + - ?z = 0"*)
1.540 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.541 + (*"z1 + z1 = 2 * z1"*)
1.542 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.543 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.544 + ], scr = EmptyScr}:rls;
1.545 +(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.546 +val discard_parentheses =
1.547 + append_rls "discard_parentheses" e_rls
1.548 + [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)),
1.549 + Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))];
1.550 +
1.551 +val scr_make_polynomial =
1.552 +"Script Expand_binoms t_ =\
1.553 +\(Repeat \
1.554 +\((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.555 +
1.556 +\ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \
1.557 +\ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \
1.558 +\ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \
1.559 +\ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \
1.560 +
1.561 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.562 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.563 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.564 +
1.565 +\ (Try (Repeat (Rewrite real_mult_commute False))) @@ \
1.566 +\ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \
1.567 +\ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \
1.568 +\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.569 +\ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \
1.570 +\ (Try (Repeat (Rewrite real_add_assoc False))) @@ \
1.571 +
1.572 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.573 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.574 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.575 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.576 +
1.577 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.578 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.579 +
1.580 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.581 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.582 +
1.583 +\ (Try (Repeat (Calculate plus ))) @@ \
1.584 +\ (Try (Repeat (Calculate times ))) @@ \
1.585 +\ (Try (Repeat (Calculate power_)))) \
1.586 +\ t_)";
1.587 +
1.588 +val make_polynomial =
1.589 + Seq{id = "make_polynomial", preconds = []:term list,
1.590 + rew_ord = ("dummy_ord", dummy_ord),
1.591 + erls = atools_erls, srls = Erls,
1.592 + calc = [],asm_thm = [],
1.593 + rules = [Rls_ expand_poly,
1.594 + Rls_ order_add_mult,
1.595 + Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
1.596 + Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
1.597 + Rls_ reduce_012,
1.598 + Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
1.599 + Rls_ discard_parentheses
1.600 + ],
1.601 + scr = EmptyScr
1.602 + }:rls;
1.603 +ruleset' := overwritel (!ruleset',
1.604 + [("expand_poly", expand_poly),
1.605 + ("simplify_power", simplify_power),
1.606 + ("order_add_mult", order_add_mult),
1.607 + ("collect_numerals", collect_numerals),
1.608 + ("reduce_012", reduce_012),
1.609 + ("discard_parentheses", discard_parentheses),
1.610 + ("make_polynomial", make_polynomial)
1.611 + ]);
1.612 +
1.613 +
1.614 +val scr_expand_binoms =
1.615 +"Script Expand_binoms t_ =\
1.616 +\(Repeat \
1.617 +\((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \
1.618 +\ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \
1.619 +\ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \
1.620 +\ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \
1.621 +\ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \
1.622 +\ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \
1.623 +
1.624 +\ (Try (Repeat (Rewrite real_mult_1 False))) @@ \
1.625 +\ (Try (Repeat (Rewrite real_mult_0 False))) @@ \
1.626 +\ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \
1.627 +
1.628 +\ (Try (Repeat (Calculate plus ))) @@ \
1.629 +\ (Try (Repeat (Calculate times ))) @@ \
1.630 +\ (Try (Repeat (Calculate power_))) @@ \
1.631 +
1.632 +\ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \
1.633 +\ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \
1.634 +\ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \
1.635 +\ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \
1.636 +
1.637 +\ (Try (Repeat (Rewrite real_num_collect False))) @@ \
1.638 +\ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \
1.639 +
1.640 +\ (Try (Repeat (Rewrite real_one_collect False))) @@ \
1.641 +\ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \
1.642 +
1.643 +\ (Try (Repeat (Calculate plus ))) @@ \
1.644 +\ (Try (Repeat (Calculate times ))) @@ \
1.645 +\ (Try (Repeat (Calculate power_)))) \
1.646 +\ t_)";
1.647 +
1.648 +val expand_binoms =
1.649 + Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.650 + erls = atools_erls, srls = Erls,
1.651 + calc = [("plus" , ("op +", eval_binop "#add_")),
1.652 + ("times" , ("op *", eval_binop "#mult_")),
1.653 + ("power_", ("Atools.pow", eval_binop "#power_"))
1.654 + ],
1.655 + asm_thm = [],
1.656 + rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.657 + (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.658 + Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.659 + (*"(a + b)*(a + b) = ...*)
1.660 + Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.661 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.662 + Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.663 + (*"(a - b)*(a - b) = ...*)
1.664 + Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.665 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.666 + Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.667 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.668 + (*RL 020915*)
1.669 + Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.670 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.671 + Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.672 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.673 + Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.674 + (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1.675 + Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.676 + (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1.677 + Thm ("realpow_multI",num_str realpow_multI),
1.678 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.679 + Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.680 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.681 + Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.682 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.683 +
1.684 +
1.685 + (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.686 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.687 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.688 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.689 + Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
1.690 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.691 + Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
1.692 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.693 + *)
1.694 +
1.695 + Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
1.696 + Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
1.697 + Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
1.698 +
1.699 + Calc ("op +", eval_binop "#add_"),
1.700 + Calc ("op *", eval_binop "#mult_"),
1.701 + Calc ("Atools.pow", eval_binop "#power_"),
1.702 + (*
1.703 + Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.704 + Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.705 + Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.706 + Thm ("real_add_commute",num_str real_add_commute), (**)
1.707 + Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
1.708 + Thm ("real_add_assoc",num_str real_add_assoc), (**)
1.709 + *)
1.710 +
1.711 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.712 + (*"r1 * r1 = r1 ^^^ 2"*)
1.713 + Thm ("realpow_plus_1",num_str realpow_plus_1),
1.714 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.715 + (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.716 + (*"z1 + z1 = 2 * z1"*)*)
1.717 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.718 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.719 +
1.720 + Thm ("real_num_collect",num_str real_num_collect),
1.721 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.722 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.723 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.724 + Thm ("real_one_collect",num_str real_one_collect),
1.725 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.726 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.727 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.728 +
1.729 + Calc ("op +", eval_binop "#add_"),
1.730 + Calc ("op *", eval_binop "#mult_"),
1.731 + Calc ("Atools.pow", eval_binop "#power_")
1.732 + ],
1.733 + scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
1.734 + }:rls;
1.735 +
1.736 +
1.737 +ruleset' := overwritel (!ruleset',
1.738 + [("make_polynomial", make_polynomial),
1.739 + ("expand_binoms", expand_binoms)
1.740 + ]);
1.741 +
1.742 +(* use"../knowledge/Poly.ML";
1.743 + use"knowledge/Poly.ML";
1.744 + use"Poly.ML";
1.745 + WN.12.8.02
1.746 + *)
1.747 +"******* Poly.ML end *******";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/Poly.thy Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,94 @@
2.4 +(* theorems in the Reals,
2.5 + necessary for special rule sets, in addition to Isabelle2002.
2.6 + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
2.7 + !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
2.8 + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
2.9 + xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
2.10 + WN.12.8.02
2.11 + changed by: rlang 02.09.12
2.12 +*)
2.13 +
2.14 +(*
2.15 + use_thy"knowledge/Poly";
2.16 + use_thy"Poly";
2.17 + use_thy_only"knowledge/Poly";
2.18 +
2.19 + remove_thy"Poly";
2.20 + use_thy"Isac";
2.21 +
2.22 +
2.23 + use"ROOT.ML";
2.24 + cd"knowledge";
2.25 + *)
2.26 +
2.27 +Poly = Atools +
2.28 +
2.29 +(*-------------------- consts-----------------------------------------------*)
2.30 +consts
2.31 +
2.32 + is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
2.33 + is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _")
2.34 + has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")
2.35 + is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")
2.36 +
2.37 + Expand'_binoms
2.38 + :: "['y, \
2.39 + \ 'y] => 'y"
2.40 + ("((Script Expand'_binoms (_ =))// \
2.41 + \ (_))" 9)
2.42 +
2.43 +(*-------------------- rules------------------------------------------------*)
2.44 +rules (*.not contained in Isabelle2002,
2.45 + stated as axioms, TODO: prove as theorems;
2.46 + theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
2.47 +
2.48 + realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
2.49 + realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
2.50 + realpow_oneI "r ^^^ 1 = r"
2.51 + realpow_eq_oneI "1 ^^^ n = 1"
2.52 + realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
2.53 + realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
2.54 +
2.55 + realpow_twoI "r ^^^ 2 = r * r"
2.56 + realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
2.57 + realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
2.58 + realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
2.59 + realpow_def_atom "[| Not (r is_atom); 1 < n |] \
2.60 + \ ==> r ^^^ n = r * r ^^^ (n + -1)"
2.61 + realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
2.62 +
2.63 +
2.64 + realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
2.65 + realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
2.66 +
2.67 +
2.68 +(* RL 020914 *)
2.69 + real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
2.70 + real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
2.71 + real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
2.72 + real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
2.73 + real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
2.74 + real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
2.75 +
2.76 + real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
2.77 + real_diff_minus "a - b = a + -1 * b"
2.78 + real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
2.79 + real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
2.80 + real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
2.81 + real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
2.82 + real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
2.83 + real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
2.84 + real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
2.85 + real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
2.86 + real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
2.87 +
2.88 + real_num_collect "[| l is_const; m is_const |] ==> \
2.89 + \l * n + m * n = (l + m) * n"
2.90 + real_num_collect_assoc "[| l is_const; m is_const |] ==> \
2.91 + \l * n + (m * n + k) = (l + m) * n + k"
2.92 + real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
2.93 + real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
2.94 +
2.95 + real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
2.96 +
2.97 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/PolyEq.ML Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,1050 @@
3.4 +(* (c) by Richard Lang
3.5 + collecting all knowledge for PolynomialEquations
3.6 + created by: rlang
3.7 + date: 02.07
3.8 + changed by: rlang
3.9 + last change by: rlang
3.10 + date: 02.11.26
3.11 +*)
3.12 +
3.13 +(* use"knowledge/PolyEq.ML";
3.14 + use"PolyEq.ML";
3.15 + use"knowledge/PolyEq.ML";
3.16 +
3.17 + use"ROOT.ML";
3.18 + cd"knowledge";
3.19 +
3.20 + remove_thy"PolyEq";
3.21 + use_thy"knowledge/Isac";
3.22 + *)
3.23 +"******* PolyEq.ML begin *******";
3.24 +
3.25 +theory' := overwritel (!theory', [("PolyEq.thy",PolyEq.thy)]);
3.26 +(*-------------------------functions---------------------*)
3.27 +local
3.28 + fun add0 l d d_ = if (d_+1) < d then add0 (str2term"0"::l) d (d_+1) else l;
3.29 + fun poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_)))) v l d =
3.30 + if (v=v_)
3.31 + then poly2list_ t1 v (((str2term("1")))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
3.32 + else t::(add0 l d 0)
3.33 + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d =
3.34 + if (v=v_)
3.35 + then poly2list_ t1 v (((t11))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
3.36 + else t::(add0 l d 0)
3.37 + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Free (v_ , _)) )) v l d =
3.38 + if (v = (str2term v_))
3.39 + then poly2list_ t1 v (((str2term("1")))::(add0 l d 1 )) 1
3.40 + else t::(add0 l d 0)
3.41 + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Free (v_,_)) ))) v l d =
3.42 + if (v= (str2term v_))
3.43 + then poly2list_ t1 v ( (t11)::(add0 l d 1 )) 1
3.44 + else t::(add0 l d 0)
3.45 + | poly2list_ (t as (Const ("op +",_) $ _ $ _))_ l d = t::(add0 l d 0)
3.46 + | poly2list_ (t as (Free (_,_))) _ l d = t::(add0 l d 0)
3.47 + | poly2list_ t _ l d = t::(add0 l d 0);
3.48 +
3.49 + fun poly2list t v = poly2list_ t v [] 0;
3.50 + fun diffpolylist_ [] _ = []
3.51 + | diffpolylist_ (x::xs) d = (str2term (if term2str(x)="0"
3.52 + then "0"
3.53 + else term2str(x)^"*"^str_of_int(d)))::diffpolylist_ xs (d+1);
3.54 + fun diffpolylist [] = []
3.55 + | diffpolylist (x::xs) = diffpolylist_ xs 1;
3.56 + (* diffpolylist(poly2list (str2term "1+ x +3*x^^^3") (str2term "x"));*)
3.57 +in
3.58 +
3.59 +end;
3.60 +(*-------------------------rulse-------------------------*)
3.61 +val polyeq_prls = (*3.10.02:just the following order due to subterm evaluation*)
3.62 + append_rls "polyeq_prls" e_rls
3.63 + [Calc ("Atools.ident",eval_ident "#ident_"),
3.64 + Calc ("Tools.matches",eval_matches ""),
3.65 + Calc ("Tools.lhs" ,eval_lhs ""),
3.66 + Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
3.67 + Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
3.68 + Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
3.69 + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
3.70 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
3.71 + Calc ("Atools.is'_const",eval_const "#is_const_"),
3.72 + Calc ("op =",eval_equal "#equal_"),
3.73 + Calc ("RootEq.is'_sqrtequation'_in",eval_is_sqrtequation_in ""),
3.74 + Calc ("RootEq.is'_rootequation'_in",eval_is_rootequation_in ""),
3.75 + Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
3.76 + Thm ("not_true",num_str not_true),
3.77 + Thm ("not_false",num_str not_false),
3.78 + Thm ("and_true",num_str and_true),
3.79 + Thm ("and_false",num_str and_false),
3.80 + Thm ("or_true",num_str or_true),
3.81 + Thm ("or_false",num_str or_false)
3.82 + (*Thm ("and_commute",num_str and_commute),
3.83 + Thm ("or_commute",num_str or_commute)*)
3.84 + ];
3.85 +
3.86 +val polyeq_erls =
3.87 + merge_rls "polyeq_erls" lineq_erls
3.88 + (append_rls "ops_preds" calculate_Rational
3.89 + [Calc ("op =",eval_equal "#equal_"),
3.90 + Thm ("plus_leq", num_str plus_leq),
3.91 + Thm ("minus_leq", num_str minus_leq),
3.92 + Thm ("rat_leq1", num_str rat_leq1),
3.93 + Thm ("rat_leq2", num_str rat_leq2),
3.94 + Thm ("rat_leq3", num_str rat_leq3)
3.95 + ]);
3.96 +
3.97 +val cancel_leading_coeff =
3.98 + Rls {id = "cancel_leading_coeff", preconds = [],
3.99 + rew_ord = ("e_rew_ord",e_rew_ord),
3.100 + erls = polyeq_erls, srls = Erls, calc = [], asm_thm = [],
3.101 + rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1),
3.102 + Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2),
3.103 + Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3),
3.104 + Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4),
3.105 + Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5),
3.106 + Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6),
3.107 + Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7),
3.108 + Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8),
3.109 + Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9),
3.110 + Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10),
3.111 + Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11),
3.112 + Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12),
3.113 + Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13)
3.114 + ],
3.115 + scr = Script ((term_of o the o (parse thy))
3.116 + "empty_script")
3.117 + }:rls;
3.118 +val complete_square =
3.119 + Rls {id = "complete_square", preconds = [],
3.120 + rew_ord = ("e_rew_ord",e_rew_ord),
3.121 + erls = polyeq_erls, srls = Erls, calc = [], asm_thm = [],
3.122 + rules = [Thm ("complete_square1",num_str complete_square1),
3.123 + Thm ("complete_square2",num_str complete_square2),
3.124 + Thm ("complete_square3",num_str complete_square3),
3.125 + Thm ("complete_square4",num_str complete_square4),
3.126 + Thm ("complete_square5",num_str complete_square5)
3.127 + ],
3.128 + scr = Script ((term_of o the o (parse thy))
3.129 + "empty_script")
3.130 + }:rls;
3.131 +ruleset' := overwritel (!ruleset',
3.132 + [("cancel_leading_coeff",cancel_leading_coeff),
3.133 + ("complete_square",complete_square),
3.134 + ("polyeq_erls",polyeq_erls)(*FIXXXME:del with rls.rls'*)
3.135 + ]);
3.136 +val poly_simplify =
3.137 + Rls {id = "poly_simplify", preconds = [],
3.138 + rew_ord = ("termlessI",termlessI),
3.139 + erls = polyeq_erls,
3.140 + srls = Erls,
3.141 + calc = [],
3.142 + asm_thm = [],
3.143 + rules = [
3.144 + Thm ("real_assoc_1",num_str real_assoc_1),
3.145 + Thm ("real_assoc_2",num_str real_assoc_2),
3.146 + Thm ("real_diff_minus",num_str real_diff_minus),
3.147 + Thm ("real_unari_minus",num_str real_unari_minus),
3.148 + Thm ("realpow_multI",num_str realpow_multI),
3.149 + Calc ("op +",eval_binop "#add_"),
3.150 + Calc ("op -",eval_binop "#sub_"),
3.151 + Calc ("op *",eval_binop "#mult_"),
3.152 + Calc ("HOL.divide", eval_cancel "#divide_"),
3.153 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
3.154 + Calc ("Atools.pow" ,eval_binop "#power_")
3.155 + ],
3.156 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.157 + }:rls;
3.158 +ruleset' := overwritel (!ruleset',
3.159 + [("poly_simplify",poly_simplify)]);
3.160 +
3.161 +val normalize_poly =
3.162 + Rls{id = "normalize_poly", preconds = [],
3.163 + rew_ord = ("termlessI",termlessI),
3.164 + erls = polyeq_erls,
3.165 + srls = Erls,
3.166 + calc = [],
3.167 + asm_thm = [],
3.168 + rules = [Thm ("all_left",num_str all_left), (* (a=b) = (a+(-1)*b=0) *)
3.169 + Thm ("makex1_x",num_str makex1_x), (* a^^^1 = a *)
3.170 + Thm ("real_assoc_1",num_str real_assoc_1), (* a+(b+c) = a+b+c *)
3.171 + Calc ("op +",eval_binop "#add_"),
3.172 + Calc ("op -",eval_binop "#sub_"),
3.173 + Calc ("op *",eval_binop "#mult_"),
3.174 + Calc ("HOL.divide", eval_cancel "#divide_"),
3.175 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
3.176 + Calc ("Atools.pow" ,eval_binop "#power_")
3.177 + ],
3.178 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.179 + }:rls;
3.180 +
3.181 +ruleset' := overwritel (!ruleset',
3.182 + [("normalize_poly", normalize_poly)
3.183 + ]);
3.184 +
3.185 +(* ------------- polySolve ------------------ *)
3.186 +(* -- d0 -- *)
3.187 +(*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
3.188 +val d0_poly_simplify =
3.189 + Rls {id = "d0_poly_simplify", preconds = [],
3.190 + rew_ord = ("e_rew_ord",e_rew_ord),
3.191 + erls = polyeq_erls,
3.192 + srls = Erls,
3.193 + calc = [],
3.194 + asm_thm = [],
3.195 + rules = [Thm("d0_true",num_str d0_true),
3.196 + Thm("d0_false",num_str d0_false)
3.197 + ],
3.198 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.199 + }:rls;
3.200 +(* -- d1 -- *)
3.201 +(*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
3.202 +val d1_poly_simplify =
3.203 + Rls {id = "d1_poly_simplify", preconds = [],
3.204 + rew_ord = ("e_rew_ord",e_rew_ord),
3.205 + erls = polyeq_erls,
3.206 + srls = Erls,
3.207 + calc = [],
3.208 + asm_thm = [("d1_isolate_div","")],
3.209 + rules = [
3.210 + Thm("d1_isolate_add1",num_str d1_isolate_add1),
3.211 + (* a+bx=0 -> bx=-a *)
3.212 + Thm("d1_isolate_add2",num_str d1_isolate_add2),
3.213 + (* a+ x=0 -> x=-a *)
3.214 + Thm("d1_isolate_div",num_str d1_isolate_div)
3.215 + (* bx=c -> x=c/b *)
3.216 + ],
3.217 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.218 + }:rls;
3.219 +(* -- d2 -- *)
3.220 +(*isolate the bound variable in an d2 equation with bdv only; 'bdv' is a meta-constant*)
3.221 +val d2_poly_bdv_only_simplify =
3.222 + Rls {id = "d2_poly_bdv_only_simplify", preconds = [],
3.223 + rew_ord = ("e_rew_ord",e_rew_ord),
3.224 + erls = polyeq_erls,
3.225 + srls = Erls,
3.226 + calc = [],
3.227 + asm_thm = [("d2_sqrt_equation1",""),("d2_isolate_div","")],
3.228 + rules = [
3.229 + Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *)
3.230 + Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *)
3.231 + Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *)
3.232 + Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *)
3.233 + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
3.234 + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
3.235 + Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*)
3.236 + Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*)
3.237 + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
3.238 + ],
3.239 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.240 + }:rls;
3.241 +(*isolate the bound variable in an d2 equation with sqrt only; 'bdv' is a meta-constant*)
3.242 +val d2_poly_sq_only_simplify =
3.243 + Rls {id = "d2_poly_sq_only_simplify", preconds = [],
3.244 + rew_ord = ("e_rew_ord",e_rew_ord),
3.245 + erls = polyeq_erls,
3.246 + srls = Erls,
3.247 + calc = [],
3.248 + asm_thm = [("d2_sqrt_equation1",""),("d2_isolate_div","")],
3.249 + rules = [
3.250 + Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*)
3.251 + Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*)
3.252 + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
3.253 + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
3.254 + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
3.255 + ],
3.256 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.257 + }:rls;
3.258 +(*isolate the bound variable in an d2 equation with pqFormula; 'bdv' is a meta-constant*)
3.259 +val d2_poly_pqFormula_simplify =
3.260 + Rls {id = "d2_poly_pqFormula_simplify", preconds = [],
3.261 + rew_ord = ("e_rew_ord",e_rew_ord),
3.262 + erls = polyeq_erls,
3.263 + srls = Erls,
3.264 + calc = [],
3.265 + asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
3.266 + ("d2_pqformula5",""),("d2_pqformula6",""),("d2_pqformula7",""),("d2_pqformula8",""),
3.267 + ("d2_pqformula9",""),("d2_pqformula10","")],
3.268 + rules = [
3.269 + Thm("d2_pqformula1",num_str d2_pqformula1), (* q+px+ x^2=0 *)
3.270 + Thm("d2_pqformula2",num_str d2_pqformula2), (* q+px+1x^2=0 *)
3.271 + Thm("d2_pqformula3",num_str d2_pqformula3), (* q+ x+ x^2=0 *)
3.272 + Thm("d2_pqformula4",num_str d2_pqformula4), (* q+ x+1x^2=0 *)
3.273 + Thm("d2_pqformula5",num_str d2_pqformula5), (* qx+ x^2=0 *)
3.274 + Thm("d2_pqformula6",num_str d2_pqformula6), (* qx+1x^2=0 *)
3.275 + Thm("d2_pqformula7",num_str d2_pqformula7), (* x+ x^2=0 *)
3.276 + Thm("d2_pqformula8",num_str d2_pqformula8), (* x+1x^2=0 *)
3.277 + Thm("d2_pqformula9",num_str d2_pqformula9), (* q +1x^2=0 *)
3.278 + Thm("d2_pqformula10",num_str d2_pqformula10), (* q + x^2=0 *)
3.279 + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *)
3.280 + Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* 1x^2=0 *)
3.281 + ],
3.282 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.283 + }:rls;
3.284 +(*isolate the bound variable in an d2 equation with abcFormula; 'bdv' is a meta-constant*)
3.285 +val d2_poly_abcFormula_simplify =
3.286 + Rls {id = "d2_poly_abcFormula_simplify", preconds = [],
3.287 + rew_ord = ("e_rew_ord",e_rew_ord),
3.288 + erls = polyeq_erls,
3.289 + srls = Erls,
3.290 + calc = [],
3.291 + asm_thm = [("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""),
3.292 + ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""),
3.293 + ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""),
3.294 + ("d2_abcformula10","")],
3.295 + rules = [
3.296 + Thm("d2_abcformula1",num_str d2_abcformula1), (*c+bx+cx^2=0 *)
3.297 + Thm("d2_abcformula2",num_str d2_abcformula2), (*c+ x+cx^2=0 *)
3.298 + Thm("d2_abcformula3",num_str d2_abcformula3), (*c+bx+ x^2=0 *)
3.299 + Thm("d2_abcformula4",num_str d2_abcformula4), (*c+ x+ x^2=0 *)
3.300 + Thm("d2_abcformula5",num_str d2_abcformula5), (*c+ cx^2=0 *)
3.301 + Thm("d2_abcformula6",num_str d2_abcformula6), (*c+ x^2=0 *)
3.302 + Thm("d2_abcformula7",num_str d2_abcformula7), (* bx+ax^2=0 *)
3.303 + Thm("d2_abcformula8",num_str d2_abcformula8), (* bx+ x^2=0 *)
3.304 + Thm("d2_abcformula9",num_str d2_abcformula9), (* x+ax^2=0 *)
3.305 + Thm("d2_abcformula10",num_str d2_abcformula10), (* x+ x^2=0 *)
3.306 + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *)
3.307 + Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* bx^2=0 *)
3.308 + ],
3.309 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.310 + }:rls;
3.311 +(*isolate the bound variable in an d2 equation; 'bdv' is a meta-constant*)
3.312 +val d2_poly_simplify =
3.313 + Rls {id = "d2_poly_simplify", preconds = [],
3.314 + rew_ord = ("e_rew_ord",e_rew_ord),
3.315 + erls = polyeq_erls,
3.316 + srls = Erls,
3.317 + calc = [],
3.318 + asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
3.319 + ("d2_abcformula1",""),("d2_abcformula2",""),("d2_sqrt_equation1",""),
3.320 + ("d2_isolate_div","")],
3.321 + rules = [
3.322 + Thm("d2_pqformula1",num_str d2_pqformula1), (* p+qx+ x^2=0 *)
3.323 + Thm("d2_pqformula2",num_str d2_pqformula2), (* p+qx+1x^2=0 *)
3.324 + Thm("d2_pqformula3",num_str d2_pqformula3), (* p+ x+ x^2=0 *)
3.325 + Thm("d2_pqformula4",num_str d2_pqformula4), (* p+ x+1x^2=0 *)
3.326 + Thm("d2_abcformula1",num_str d2_abcformula1), (* c+bx+cx^2=0 *)
3.327 + Thm("d2_abcformula2",num_str d2_abcformula2), (* c+ x+cx^2=0 *)
3.328 + Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *)
3.329 + Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *)
3.330 + Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *)
3.331 + Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *)
3.332 + Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*)
3.333 + Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*)
3.334 + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
3.335 + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
3.336 + Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*)
3.337 + Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*)
3.338 + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
3.339 + ],
3.340 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.341 + }:rls;
3.342 +(* -- d3 -- *)
3.343 +(*isolate the bound variable in an d3 equation; 'bdv' is a meta-constant*)
3.344 +val d3_poly_simplify =
3.345 + Rls {id = "d3_poly_simplify", preconds = [],
3.346 + rew_ord = ("e_rew_ord",e_rew_ord),
3.347 + erls = polyeq_erls,
3.348 + srls = Erls,
3.349 + calc = [],
3.350 + asm_thm = [("d3_isolate_div","")],
3.351 + rules = [
3.352 + Thm("d3_reduce_equation1",num_str d3_reduce_equation1),
3.353 + (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
3.354 + Thm("d3_reduce_equation2",num_str d3_reduce_equation2),
3.355 + (* bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
3.356 + Thm("d3_reduce_equation3",num_str d3_reduce_equation3),
3.357 + (*a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
3.358 + Thm("d3_reduce_equation4",num_str d3_reduce_equation4),
3.359 + (* bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
3.360 + Thm("d3_reduce_equation5",num_str d3_reduce_equation5),
3.361 + (*a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
3.362 + Thm("d3_reduce_equation6",num_str d3_reduce_equation6),
3.363 + (* bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
3.364 + Thm("d3_reduce_equation7",num_str d3_reduce_equation7),
3.365 + (*a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*)
3.366 + Thm("d3_reduce_equation8",num_str d3_reduce_equation8),
3.367 + (* bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*)
3.368 + Thm("d3_reduce_equation9",num_str d3_reduce_equation9),
3.369 + (*a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0)*)
3.370 + Thm("d3_reduce_equation10",num_str d3_reduce_equation10),
3.371 + (* bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0)*)
3.372 + Thm("d3_reduce_equation11",num_str d3_reduce_equation11),
3.373 + (*a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0)*)
3.374 + Thm("d3_reduce_equation12",num_str d3_reduce_equation12),
3.375 + (* bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0)*)
3.376 + Thm("d3_reduce_equation13",num_str d3_reduce_equation13),
3.377 + (* b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
3.378 + Thm("d3_reduce_equation14",num_str d3_reduce_equation14),
3.379 + (* bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0)*)
3.380 + Thm("d3_reduce_equation15",num_str d3_reduce_equation15),
3.381 + (* b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0)*)
3.382 + Thm("d3_reduce_equation16",num_str d3_reduce_equation16),
3.383 + (* bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0)*)
3.384 + Thm("d3_isolate_add1",num_str d3_isolate_add1),
3.385 + (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (bdv=0 | (b*bdv^^^3=a)*)
3.386 + Thm("d3_isolate_add2",num_str d3_isolate_add2),
3.387 + (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = (bdv=0 | ( bdv^^^3=a)*)
3.388 + Thm("d3_isolate_div",num_str d3_isolate_div),
3.389 + (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
3.390 + Thm("d3_root_equation2",num_str d3_root_equation2),
3.391 + (*(bdv^^^3=0) = (bdv=0) *)
3.392 + Thm("d3_root_equation1",num_str d3_root_equation1)
3.393 + (*bdv^^^3=c) = (bdv = nroot 3 c*)
3.394 + ],
3.395 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.396 + }:rls;
3.397 +(* -- d4 -- *)
3.398 +(*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
3.399 +val d4_poly_simplify =
3.400 + Rls {id = "d4_poly_simplify", preconds = [],
3.401 + rew_ord = ("e_rew_ord",e_rew_ord),
3.402 + erls = polyeq_erls,
3.403 + srls = Erls,
3.404 + calc = [],
3.405 + asm_thm = [],
3.406 + rules = [Thm("d4_sub_u1",num_str d4_sub_u1)
3.407 + (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
3.408 + ],
3.409 + scr = Script ((term_of o the o (parse thy)) "empty_script")
3.410 + }:rls;
3.411 +
3.412 +ruleset' := overwritel (!ruleset',
3.413 + [("d0_poly_simplify", d0_poly_simplify),
3.414 + ("d1_poly_simplify", d1_poly_simplify),
3.415 + ("d2_poly_simplify", d2_poly_simplify),
3.416 + ("d2_poly_bdv_only_simplify", d2_poly_bdv_only_simplify),
3.417 + ("d2_poly_sq_only_simplify", d2_poly_sq_only_simplify),
3.418 + ("d2_poly_pqFormula_simplify", d2_poly_pqFormula_simplify),
3.419 + ("d2_poly_abcFormula_simplify", d2_poly_abcFormula_simplify),
3.420 + ("d3_poly_simplify", d3_poly_simplify),
3.421 + ("d4_poly_simplify", d4_poly_simplify)
3.422 + ]);
3.423 +
3.424 +(*------------------------probleme------------------------*)
3.425 +(*
3.426 +(get_pbt ["degree_2","polynomial","univariate","equation"]);
3.427 +show_ptyps();
3.428 +*)
3.429 +
3.430 +(*-------------------------poly-----------------------*)
3.431 +store_pbt
3.432 + (prep_pbt PolyEq.thy
3.433 + (["polynomial","univariate","equation"],
3.434 + [("#Given" ,["equality e_","solveFor v_"]),
3.435 + ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))",
3.436 + "~((lhs e_) is_rootequation_in (v_::real))",
3.437 + "~((rhs e_) is_rootequation_in (v_::real))"]),
3.438 + ("#Find" ,["solutions v_i_"])
3.439 + ],
3.440 + polyeq_prls, None,
3.441 + []));
3.442 +(*--- d0 ---*)
3.443 +store_pbt
3.444 + (prep_pbt PolyEq.thy
3.445 + (["degree_0","polynomial","univariate","equation"],
3.446 + [("#Given" ,["equality e_","solveFor v_"]),
3.447 + ("#Where" ,["matches (?a = 0) e_",
3.448 + "(lhs e_) is_poly_in v_",
3.449 + "((lhs e_) has_degree_in v_ ) = 0"
3.450 + ]),
3.451 + ("#Find" ,["solutions v_i_"])
3.452 + ],
3.453 + polyeq_prls, None,
3.454 + [("PolyEq.thy","solve_d0_poly_equation")]));
3.455 +
3.456 +(*--- d1 ---*)
3.457 +store_pbt
3.458 + (prep_pbt PolyEq.thy
3.459 + (["degree_1","polynomial","univariate","equation"],
3.460 + [("#Given" ,["equality e_","solveFor v_"]),
3.461 + ("#Where" ,["matches (?a = 0) e_",
3.462 + "(lhs e_) is_poly_in v_",
3.463 + "((lhs e_) has_degree_in v_ ) = 1"
3.464 + ]),
3.465 + ("#Find" ,["solutions v_i_"])
3.466 + ],
3.467 + polyeq_prls, None,
3.468 + [("PolyEq.thy","solve_d1_poly_equation")]));
3.469 +
3.470 +(*--- d2 ---*)
3.471 +store_pbt
3.472 + (prep_pbt PolyEq.thy
3.473 + (["degree_2","polynomial","univariate","equation"],
3.474 + [("#Given" ,["equality e_","solveFor v_"]),
3.475 + ("#Where" ,["matches (?a = 0) e_",
3.476 + "(lhs e_) is_poly_in v_ ",
3.477 + "((lhs e_) has_degree_in v_ ) = 2"]),
3.478 + ("#Find" ,["solutions v_i_"])
3.479 + ],
3.480 + polyeq_prls, None,
3.481 + [("PolyEq.thy","solve_d2_poly_equation")]));
3.482 +
3.483 + store_pbt
3.484 + (prep_pbt PolyEq.thy
3.485 + (["sq_only","degree_2","polynomial","univariate","equation"],
3.486 + [("#Given" ,["equality e_","solveFor v_"]),
3.487 + ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | \
3.488 + \matches ( ?a + ?b*?v_^^^2 = 0) e_ | \
3.489 + \matches ( ?v_^^^2 = 0) e_ | \
3.490 + \matches ( ?b*?v_^^^2 = 0) e_" ,
3.491 + "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &\
3.492 + \Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &\
3.493 + \Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &\
3.494 + \Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &\
3.495 + \Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &\
3.496 + \Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &\
3.497 + \Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &\
3.498 + \Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]),
3.499 + ("#Find" ,["solutions v_i_"])
3.500 + ],
3.501 + polyeq_prls, None,
3.502 + [("PolyEq.thy","solve_d2_poly_sqonly_equation")]));
3.503 +
3.504 +store_pbt
3.505 + (prep_pbt PolyEq.thy
3.506 + (["bdv_only","degree_2","polynomial","univariate","equation"],
3.507 + [("#Given" ,["equality e_","solveFor v_"]),
3.508 + ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | \
3.509 + \matches ( ?v_ + ?v_^^^2 = 0) e_ | \
3.510 + \matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | \
3.511 + \matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | \
3.512 + \matches ( ?v_^^^2 = 0) e_ | \
3.513 + \matches ( ?b*?v_^^^2 = 0) e_ "]),
3.514 + ("#Find" ,["solutions v_i_"])
3.515 + ],
3.516 + polyeq_prls, None,
3.517 + [("PolyEq.thy","solve_d2_poly_bdvonly_equation")]));
3.518 +
3.519 +store_pbt
3.520 + (prep_pbt PolyEq.thy
3.521 + (["pqFormula","degree_2","polynomial","univariate","equation"],
3.522 + [("#Given" ,["equality e_","solveFor v_"]),
3.523 + ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | \
3.524 + \matches (?a + ?v_^^^2 = 0) e_"]),
3.525 + ("#Find" ,["solutions v_i_"])
3.526 + ],
3.527 + polyeq_prls, None,
3.528 + [("PolyEq.thy","solve_d2_poly_pq_equation")]));
3.529 +
3.530 +store_pbt
3.531 + (prep_pbt PolyEq.thy
3.532 + (["abcFormula","degree_2","polynomial","univariate","equation"],
3.533 + [("#Given" ,["equality e_","solveFor v_"]),
3.534 + ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | \
3.535 + \matches (?a + ?b*?v_^^^2 = 0) e_"]),
3.536 + ("#Find" ,["solutions v_i_"])
3.537 + ],
3.538 + polyeq_prls, None,
3.539 + [("PolyEq.thy","solve_d2_poly_abc_equation")]));
3.540 +
3.541 +(*--- d3 ---*)
3.542 +store_pbt
3.543 + (prep_pbt PolyEq.thy
3.544 + (["degree_3","polynomial","univariate","equation"],
3.545 + [("#Given" ,["equality e_","solveFor v_"]),
3.546 + ("#Where" ,["matches (?a = 0) e_",
3.547 + "(lhs e_) is_poly_in v_ ",
3.548 + "((lhs e_) has_degree_in v_) = 3"]),
3.549 + ("#Find" ,["solutions v_i_"])
3.550 + ],
3.551 + polyeq_prls, None,
3.552 + [("PolyEq.thy","solve_d3_poly_equation")]));
3.553 +
3.554 +(*--- d4 ---*)
3.555 +store_pbt
3.556 + (prep_pbt PolyEq.thy
3.557 + (["degree_4","polynomial","univariate","equation"],
3.558 + [("#Given" ,["equality e_","solveFor v_"]),
3.559 + ("#Where" ,["matches (?a = 0) e_",
3.560 + "(lhs e_) is_poly_in v_ ",
3.561 + "((lhs e_) has_degree_in v_) = 4"]),
3.562 + ("#Find" ,["solutions v_i_"])
3.563 + ],
3.564 + polyeq_prls, None,
3.565 + [("PolyEq.thy","solve_d4_poly_equation")]));
3.566 +
3.567 +(*--- normalize ---*)
3.568 +store_pbt
3.569 + (prep_pbt PolyEq.thy
3.570 + (["normalize","polynomial","univariate","equation"],
3.571 + [("#Given" ,["equality e_","solveFor v_"]),
3.572 + ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\
3.573 + \(Not(((lhs e_) is_poly_in v_)))"]),
3.574 + ("#Find" ,["solutions v_i_"])
3.575 + ],
3.576 + polyeq_prls, None,
3.577 + [("PolyEq.thy","normalize_poly")]));
3.578 +(*-------------------------expanded-----------------------*)
3.579 +store_pbt
3.580 + (prep_pbt PolyEq.thy
3.581 + (["expanded","univariate","equation"],
3.582 + [("#Given" ,["equality e_","solveFor v_"]),
3.583 + ("#Where" ,["matches (?a = 0) e_",
3.584 + "(lhs e_) is_expanded_in v_ "]),
3.585 + ("#Find" ,["solutions v_i_"])
3.586 + ],
3.587 + polyeq_prls, None,
3.588 + []));
3.589 +
3.590 +(*--- d2 ---*)
3.591 +store_pbt
3.592 + (prep_pbt PolyEq.thy
3.593 + (["degree_2","expanded","univariate","equation"],
3.594 + [("#Given" ,["equality e_","solveFor v_"]),
3.595 + ("#Where" ,["((lhs e_) has_degree_in v_) = 2"]),
3.596 + ("#Find" ,["solutions v_i_"])
3.597 + ],
3.598 + polyeq_prls, None,
3.599 + [("PolyEq.thy","complete_square")]));
3.600 +
3.601 +(*-------------------------Methode-----------------------*)
3.602 +methods:= overwritel (!methods,
3.603 +[
3.604 + prep_met
3.605 + (("PolyEq.thy","normalize_poly"),
3.606 + [("#Given" ,["equality e_","solveFor v_"]),
3.607 + ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\
3.608 + \(Not(((lhs e_) is_poly_in v_)))"]),
3.609 + ("#Find" ,["solutions v_i_"])
3.610 + ],
3.611 + {rew_ord'="termlessI",
3.612 + rls'=polyeq_erls,
3.613 + srls=e_rls,
3.614 + prls=polyeq_prls,
3.615 + calc=[],
3.616 + asm_rls=[],asm_thm=[]},
3.617 + "Script Normalize_poly (e_::bool) (v_::real) = \
3.618 + \(let e_ =((Try (Rewrite all_left False)) @@ \
3.619 + \ (Try (Repeat (Rewrite makex1_x False))) @@ \
3.620 + \ (Try (Repeat (Rewrite_Set expand_binoms False))) @@ \
3.621 + \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
3.622 + \ make_ratpoly_in False))) @@ \
3.623 + \ (Try (Repeat (Rewrite_Set poly_simplify False)))) e_ \
3.624 + \ in (SubProblem (PolyEq_,[polynomial,univariate,equation], \
3.625 + \ (PolyEq_,no_met)) [bool_ e_, real_ v_]))"
3.626 + )
3.627 +,
3.628 +prep_met
3.629 + (("PolyEq.thy","solve_d0_poly_equation"),
3.630 + [("#Given" ,["equality e_","solveFor v_"]),
3.631 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.632 + "((lhs e_) has_degree_in v_) = 0"]),
3.633 + ("#Find" ,["solutions v_i_"])
3.634 + ],
3.635 + {rew_ord'="termlessI",
3.636 + rls'=polyeq_erls,
3.637 + srls=e_rls,
3.638 + prls=polyeq_prls,
3.639 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.640 + asm_rls=[],asm_thm=[]},
3.641 + "Script Solve_d0_poly_equation (e_::bool) (v_::real) = \
3.642 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d0_poly_simplify False))) e_ \
3.643 + \ in ((Or_to_List e_)::bool list))"
3.644 + )
3.645 +,
3.646 +prep_met
3.647 + (("PolyEq.thy","solve_d1_poly_equation"),
3.648 + [("#Given" ,["equality e_","solveFor v_"]),
3.649 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.650 + "((lhs e_) has_degree_in v_) = 1"]),
3.651 + ("#Find" ,["solutions v_i_"])
3.652 + ],
3.653 + {rew_ord'="termlessI",
3.654 + rls'=polyeq_erls,
3.655 + srls=e_rls,
3.656 + prls=polyeq_prls,
3.657 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.658 + asm_rls=["d1_poly_simplify"],
3.659 + asm_thm=[("d1_isolate_div","")]},
3.660 + "Script Solve_d1_poly_equation (e_::bool) (v_::real) = \
3.661 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_poly_simplify True)) @@ \
3.662 + \ (Try (Rewrite_Set poly_simplify False))) e_; \
3.663 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.664 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.665 + )
3.666 +,
3.667 +prep_met
3.668 + (("PolyEq.thy","solve_d2_poly_equation"),
3.669 + [("#Given" ,["equality e_","solveFor v_"]),
3.670 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.671 + "((lhs e_) has_degree_in v_) = 2"]),
3.672 + ("#Find" ,["solutions v_i_"])
3.673 + ],
3.674 + {rew_ord'="termlessI",
3.675 + rls'=polyeq_erls,
3.676 + srls=e_rls,
3.677 + prls=polyeq_prls,
3.678 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.679 + asm_rls=["d2_poly_simplify","d1_poly_simplify"],
3.680 + asm_thm = [("d1_isolate_div",""),("d2_pqformula1",""),("d2_pqformula2",""),
3.681 + ("d2_pqformula3",""),("d2_pqformula4",""),("d2_abcformula1",""),
3.682 + ("d2_abcformula2",""),("d2_sqrt_equation1",""),("d2_isolate_div","")]},
3.683 + "Script Solve_d2_poly_equation (e_::bool) (v_::real) = \
3.684 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d2_poly_simplify True)) @@ \
3.685 + \ (Try (Rewrite_Set poly_simplify False)) @@ \
3.686 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_poly_simplify True)) @@ \
3.687 + \ (Try (Rewrite_Set poly_simplify False))) e_;\
3.688 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.689 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.690 + )
3.691 +,
3.692 +prep_met
3.693 + (("PolyEq.thy","solve_d2_poly_bdvonly_equation"),
3.694 + [("#Given" ,["equality e_","solveFor v_"]),
3.695 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.696 + "((lhs e_) has_degree_in v_) = 2"]),
3.697 + ("#Find" ,["solutions v_i_"])
3.698 + ],
3.699 + {rew_ord'="termlessI",
3.700 + rls'=polyeq_erls,
3.701 + srls=e_rls,
3.702 + prls=polyeq_prls,
3.703 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.704 + asm_rls=["d2_poly_bdv_only_simplify","d1_poly_simplify "],
3.705 + asm_thm=[("d1_isolate_div",""),("d2_isolate_div",""),
3.706 + ("d2_sqrt_equation1","")]},
3.707 + "Script Solve_d2_poly_bdvonly_equation (e_::bool) (v_::real) =\
3.708 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
3.709 + \ d2_poly_bdv_only_simplify True)) @@ \
3.710 + \ (Try (Rewrite_Set poly_simplify False)) @@ \
3.711 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
3.712 + \ d1_poly_simplify True)) @@ \
3.713 + \ (Try (Rewrite_Set poly_simplify False))) e_; \
3.714 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.715 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.716 + )
3.717 +,
3.718 +prep_met
3.719 + (("PolyEq.thy","solve_d2_poly_sqonly_equation"),
3.720 + [("#Given" ,["equality e_","solveFor v_"]),
3.721 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.722 + "((lhs e_) has_degree_in v_) = 2"]),
3.723 + ("#Find" ,["solutions v_i_"])
3.724 + ],
3.725 + {rew_ord'="termlessI",
3.726 + rls'=polyeq_erls,
3.727 + srls=e_rls,
3.728 + prls=polyeq_prls,
3.729 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.730 + asm_rls=["d2_poly_sq_only_simplify"],
3.731 + asm_thm=[("d2_sqrt_equation1",""),("d2_isolate_div","")]},
3.732 + "Script Solve_d2_poly_sqonly_equation (e_::bool) (v_::real) = \
3.733 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
3.734 + \ d2_poly_sq_only_simplify True)) @@ \
3.735 + \ (Try (Rewrite_Set poly_simplify False))) e_; \
3.736 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.737 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.738 + )
3.739 +,
3.740 +prep_met
3.741 + (("PolyEq.thy","solve_d2_poly_pq_equation"),
3.742 + [("#Given" ,["equality e_","solveFor v_"]),
3.743 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.744 + "((lhs e_) has_degree_in v_) = 2"]),
3.745 + ("#Find" ,["solutions v_i_"])
3.746 + ],
3.747 + {rew_ord'="termlessI",
3.748 + rls'=polyeq_erls,
3.749 + srls=e_rls,
3.750 + prls=polyeq_prls,
3.751 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.752 + asm_rls=["d2_poly_pqFormula_simplify"],
3.753 + asm_thm=[("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),
3.754 + ("d2_pqformula4",""),("d2_pqformula5",""),("d2_pqformula6",""),
3.755 + ("d2_pqformula7",""),("d2_pqformula8",""),("d2_pqformula9",""),
3.756 + ("d2_pqformula10","")]},
3.757 + "Script Solve_d2_poly_pq_equation (e_::bool) (v_::real) = \
3.758 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
3.759 + \ d2_poly_pqFormula_simplify True)) @@ \
3.760 + \ (Try (Rewrite_Set poly_simplify False))) e_;\
3.761 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.762 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.763 + )
3.764 +,
3.765 +prep_met
3.766 + (("PolyEq.thy","solve_d2_poly_abc_equation"),
3.767 + [("#Given" ,["equality e_","solveFor v_"]),
3.768 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.769 + "((lhs e_) has_degree_in v_) = 2"]),
3.770 + ("#Find" ,["solutions v_i_"])
3.771 + ],
3.772 + {rew_ord'="termlessI",
3.773 + rls'=polyeq_erls,
3.774 + srls=e_rls,
3.775 + prls=polyeq_prls,
3.776 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.777 + asm_rls=["d2_poly_abcFormula_simplify"],
3.778 + asm_thm=[("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""),
3.779 + ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""),
3.780 + ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""),
3.781 + ("d2_abcformula10","")]},
3.782 + "Script Solve_d2_poly_abc_equation (e_::bool) (v_::real) = \
3.783 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
3.784 + \ d2_poly_abcFormula_simplify True)) @@ \
3.785 + \ (Try (Rewrite_Set poly_simplify False))) e_;\
3.786 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.787 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.788 + )
3.789 +,
3.790 +prep_met
3.791 + (("PolyEq.thy","solve_d3_poly_equation"),
3.792 + [("#Given" ,["equality e_","solveFor v_"]),
3.793 + ("#Where" ,["(lhs e_) is_poly_in v_ ",
3.794 + "((lhs e_) has_degree_in v_) = 3"]),
3.795 + ("#Find" ,["solutions v_i_"])
3.796 + ],
3.797 + {rew_ord'="termlessI",
3.798 + rls'=polyeq_erls,
3.799 + srls=e_rls,
3.800 + prls=polyeq_prls,
3.801 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.802 + asm_rls=["d1_poly_simplify","d2_poly_simplify","d1_poly_simplify"],
3.803 + asm_thm=[("d3_isolate_div",""),("d1_isolate_div",""),("d2_pqformula1",""),
3.804 + ("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
3.805 + ("d2_abcformula1",""),("d2_abcformula2",""),("d2_sqrt_equation1",""),
3.806 + ("d2_isolate_div","")]},
3.807 + "Script Solve_d3_poly_equation (e_::bool) (v_::real) = \
3.808 + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] d3_poly_simplify True)) @@ \
3.809 + \ (Try (Rewrite_Set poly_simplify False)) @@ \
3.810 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d2_poly_simplify True)) @@ \
3.811 + \ (Try (Rewrite_Set poly_simplify False)) @@ \
3.812 + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] d1_poly_simplify True)) @@ \
3.813 + \ (Try (Rewrite_Set poly_simplify False))) e_;\
3.814 + \ (L_::bool list) = ((Or_to_List e_)::bool list) \
3.815 + \ in Check_elementwise L_ {(v_::real). Assumptions} )"
3.816 + )
3.817 + ,
3.818 + (*.solves all expanded (ie. normalized) terms of degree 2.*)
3.819 + (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
3.820 + by 'polyeq_erls'; restricted until Float.thy is implemented*)
3.821 + prep_met
3.822 + (("PolyEq.thy","complete_square"),
3.823 + [("#Given" ,["equality e_","solveFor v_"]),
3.824 + ("#Where" ,["matches (?a = 0) e_",
3.825 + "((lhs e_) has_degree_in v_) = 2"]),
3.826 + ("#Find" ,["solutions v_i_"])
3.827 + ],
3.828 + {rew_ord'="termlessI",rls'=polyeq_erls,srls=e_rls,prls=polyeq_prls,
3.829 + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
3.830 + asm_rls=[],asm_thm=[("root_plus_minus","")]},
3.831 + "Script Complete_square (e_::bool) (v_::real) = \
3.832 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\
3.833 + \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \
3.834 + \ @@ (Try (Rewrite square_explicit1 False)) \
3.835 + \ @@ (Try (Rewrite square_explicit2 False)) \
3.836 + \ @@ (Rewrite root_plus_minus True) \
3.837 + \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) \
3.838 + \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \
3.839 + \ @@ (Try (Repeat \
3.840 + \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \
3.841 + \ @@ (Try (Rewrite_Set calculate_RootRat False)) \
3.842 + \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \
3.843 + \ in ((Or_to_List e_)::bool list))"
3.844 + )
3.845 + ]);
3.846 +(*6.10.02: x^2=64: root_plus_minus -/-/->
3.847 + "Script Complete_square (e_::bool) (v_::real) = \
3.848 + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\
3.849 + \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \
3.850 + \ @@ (Try ((Rewrite square_explicit1 False) \
3.851 + \ Or (Rewrite square_explicit2 False))) \
3.852 + \ @@ (Rewrite root_plus_minus True) \
3.853 + \ @@ ((Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False)) \
3.854 + \ Or (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \
3.855 + \ @@ (Try (Repeat \
3.856 + \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \
3.857 + \ @@ (Try (Rewrite_Set calculate_RootRat False)) \
3.858 + \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \
3.859 + \ in ((Or_to_List e_)::bool list))"*)
3.860 +
3.861 +"******* PolyEq.ML end *******";
3.862 +
3.863 +(*eine gehackte termorder*)
3.864 +local (*. for make_polynomial_in .*)
3.865 +
3.866 +open Term; (* for type order = EQUAL | LESS | GREATER *)
3.867 +
3.868 +fun pr_ord EQUAL = "EQUAL"
3.869 + | pr_ord LESS = "LESS"
3.870 + | pr_ord GREATER = "GREATER";
3.871 +
3.872 +fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
3.873 + | dest_hd' x (t as Free (a, T)) =
3.874 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
3.875 + else (((a, 0), T), 1)
3.876 + | dest_hd' x (Var v) = (v, 2)
3.877 + | dest_hd' x (Bound i) = ((("", i), dummyT), 3)
3.878 + | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
3.879 +
3.880 +fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
3.881 + (case x of (*WN*)
3.882 + (Free (xstr,_)) =>
3.883 + (if xstr = var then 1000*(the (int_of_str pot)) else 3)
3.884 + | _ => raise error ("size_of_term' called with subst = "^
3.885 + (term2str x)))
3.886 + | size_of_term' x (Free (subst,_)) =
3.887 + (case x of
3.888 + (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
3.889 + | _ => raise error ("size_of_term' called with subst = "^
3.890 + (term2str x)))
3.891 + | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
3.892 + | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
3.893 + | size_of_term' x _ = 1;
3.894 +
3.895 +(*
3.896 +fun size_of_term'MG x (t1 $ t2) =
3.897 +(* if x = t2 then 1000 + size_of_term' x t1 else 1 + size_of_term' x t1 *)(*WN*)
3.898 +if x = t2 then 1000 + size_of_term' x t1 else size_of_term' x t1 + size_of_term' x t2 (*MG*)
3.899 + | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
3.900 + | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
3.901 + | size_of_term' x _ = 1;
3.902 +*)
3.903 +
3.904 +fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
3.905 + (case term_ord' x pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
3.906 + | term_ord' x pr thy (t, u) =
3.907 + (if pr then
3.908 + let
3.909 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
3.910 + val _=writeln("t= f@ts= \""^
3.911 + ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
3.912 + (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
3.913 + val _=writeln("u= g@us= \""^
3.914 + ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
3.915 + (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
3.916 + val _=writeln("size_of_term(t,u)= ("^
3.917 + (string_of_int(size_of_term' x t))^", "^
3.918 + (string_of_int(size_of_term' x u))^")");
3.919 + val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
3.920 + val _=writeln("terms_ord(ts,us) = "^
3.921 + ((pr_ord o (terms_ord x) str false)(ts,us)));
3.922 + val _=writeln("-------");
3.923 + in () end
3.924 + else ();
3.925 + case int_ord (size_of_term' x t, size_of_term' x u) of
3.926 + EQUAL =>
3.927 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
3.928 + (case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us)
3.929 + | ord => ord)
3.930 + end
3.931 + | ord => ord)
3.932 +and hd_ord x (f, g) = (* ~ term.ML *)
3.933 + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f,
3.934 + dest_hd' x g)
3.935 +and terms_ord x str pr (ts, us) =
3.936 + list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
3.937 +(*val x = (term_of o the o (parse thy)) "x"; (*FIXXXXXXME*)
3.938 +*)
3.939 +
3.940 +in
3.941 +
3.942 +fun ord_make_polynomial_in (pr:bool) thy subst tu =
3.943 + let
3.944 + (* val _=writeln("*** subs variable is: "^(subst2str subst)); *)
3.945 + in
3.946 + case subst of
3.947 + (_,x)::_ => (term_ord' x pr thy tu = LESS)
3.948 + | _ => raise error ("ord_make_polynomial_in called with subst = "^
3.949 + (subst2str subst))
3.950 + end;
3.951 +end;
3.952 +
3.953 +val order_add_mult_in =
3.954 + Rls{id = "order_add_mult_in", preconds = [],
3.955 + rew_ord = ("ord_make_polynomial_in",
3.956 + ord_make_polynomial_in false Poly.thy),
3.957 + erls = e_rls,srls = Erls,
3.958 + calc = [],
3.959 + asm_thm = [],
3.960 + rules = [Thm ("real_mult_commute",num_str real_mult_commute),
3.961 + (* z * w = w * z *)
3.962 + Thm ("real_mult_left_commute",num_str real_mult_left_commute),
3.963 + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
3.964 + Thm ("real_mult_assoc",num_str real_mult_assoc),
3.965 + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
3.966 + Thm ("real_add_commute",num_str real_add_commute),
3.967 + (*z + w = w + z*)
3.968 + Thm ("real_add_left_commute",num_str real_add_left_commute),
3.969 + (*x + (y + z) = y + (x + z)*)
3.970 + Thm ("real_add_assoc",num_str real_add_assoc)
3.971 + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
3.972 + ], scr = EmptyScr}:rls;
3.973 +
3.974 +val collect_bdv =
3.975 + Rls{id = "collect_bdv", preconds = [],
3.976 + rew_ord = ("dummy_ord", dummy_ord),
3.977 + erls = e_rls,srls = Erls,
3.978 + calc = [],
3.979 + asm_thm = [],
3.980 + rules = [Thm ("bdv_collect_1",num_str bdv_collect_1),
3.981 + Thm ("bdv_collect_2",num_str bdv_collect_2),
3.982 + Thm ("bdv_collect_3",num_str bdv_collect_3),
3.983 +
3.984 + Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1),
3.985 + Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2),
3.986 + Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3),
3.987 +
3.988 + Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1),
3.989 + Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2),
3.990 + Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3),
3.991 +
3.992 +
3.993 + Thm ("bdv_n_collect_1",num_str bdv_n_collect_1),
3.994 + Thm ("bdv_n_collect_2",num_str bdv_n_collect_2),
3.995 + Thm ("bdv_n_collect_3",num_str bdv_n_collect_3),
3.996 +
3.997 + Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1),
3.998 + Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2),
3.999 + Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3),
3.1000 +
3.1001 + Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1),
3.1002 + Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2),
3.1003 + Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3)
3.1004 + ], scr = EmptyScr}:rls;
3.1005 +
3.1006 +(*.transforms an arbitrary term without roots to a polynomial [4]
3.1007 + according to knowledge/Poly.sml.*)
3.1008 +val make_polynomial_in =
3.1009 + Seq {id = "make_polynomial_in", preconds = []:term list,
3.1010 + rew_ord = ("dummy_ord", dummy_ord),
3.1011 + erls = atools_erls, srls = Erls,
3.1012 + calc = [], asm_thm = [],
3.1013 + rules = [Rls_ expand_poly,
3.1014 + Rls_ order_add_mult_in,
3.1015 + Rls_ simplify_power,
3.1016 + Rls_ collect_numerals,
3.1017 + Rls_ reduce_012,
3.1018 + Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
3.1019 + Rls_ discard_parentheses,
3.1020 + Rls_ collect_bdv
3.1021 + ],
3.1022 + scr = EmptyScr
3.1023 + }:rls;
3.1024 +val make_ratpoly_in =
3.1025 + Seq {id = "make_ratpoly_in", preconds = []:term list,
3.1026 + rew_ord = ("dummy_ord", dummy_ord),
3.1027 + erls = atools_erls, srls = Erls,
3.1028 + calc = [], asm_thm = [],
3.1029 + rules = [Rls_ norm_Rational,
3.1030 + Rls_ order_add_mult_in,
3.1031 + Rls_ discard_parentheses,
3.1032 + Rls_ (append_rls "separate_bdv"
3.1033 + collect_bdv
3.1034 + [Thm ("separate_bdv", num_str separate_bdv),
3.1035 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
3.1036 + Thm ("separate_bdv_n", num_str separate_bdv_n),
3.1037 + Thm ("separate_1_bdv", num_str separate_1_bdv),
3.1038 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
3.1039 + Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
3.1040 + Thm ("real_add_divide_distrib",
3.1041 + num_str real_add_divide_distrib)
3.1042 + ]),
3.1043 + Calc ("HOL.divide" ,eval_cancel "#divide_")
3.1044 + ],
3.1045 + scr = EmptyScr}:rls;
3.1046 +
3.1047 +ruleset' := overwritel (!ruleset',
3.1048 + [("order_add_mult_in", order_add_mult_in),
3.1049 + ("collect_bdv", collect_bdv),
3.1050 + ("make_polynomial_in", make_polynomial_in),
3.1051 + ("make_ratpoly_in", make_ratpoly_in)
3.1052 + ]);
3.1053 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/IsacKnowledge/PolyEq.thy Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,366 @@
4.4 +(* (c) by Richard Lang
4.5 + theory collecting all knowledge
4.6 + (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
4.7 + for PolynomialEquations.
4.8 + alternative dependencies see Isac.thy
4.9 + created by: rlang
4.10 + date: 02.07
4.11 + changed by: rlang
4.12 + last change by: rlang
4.13 + date: 02.11.26
4.14 + (c) Richard Lang, 2003
4.15 +*)
4.16 +
4.17 +(* remove_thy"PolyEq";
4.18 + use_thy"knowledge/Isac";
4.19 + use_thy"knowledge/PolyEq";
4.20 +
4.21 + remove_thy"PolyEq";
4.22 + use_thy"Isac";
4.23 +
4.24 + use"ROOT.ML";
4.25 + cd"knowledge";
4.26 + *)
4.27 +
4.28 +PolyEq = LinEq + RootRatEq +
4.29 +(*-------------------- consts ------------------------------------------------*)
4.30 +consts
4.31 +
4.32 +(*---------scripts--------------------------*)
4.33 + Complete'_square
4.34 + :: "[bool,real, \
4.35 + \ bool list] => bool list"
4.36 + ("((Script Complete'_square (_ _ =))// \
4.37 + \ (_))" 9)
4.38 + (*----- poly ----- *)
4.39 + Normalize'_poly
4.40 + :: "[bool,real, \
4.41 + \ bool list] => bool list"
4.42 + ("((Script Normalize'_poly (_ _=))// \
4.43 + \ (_))" 9)
4.44 + Solve'_d0'_poly'_equation
4.45 + :: "[bool,real, \
4.46 + \ bool list] => bool list"
4.47 + ("((Script Solve'_d0'_poly'_equation (_ _ =))// \
4.48 + \ (_))" 9)
4.49 + Solve'_d1'_poly'_equation
4.50 + :: "[bool,real, \
4.51 + \ bool list] => bool list"
4.52 + ("((Script Solve'_d1'_poly'_equation (_ _ =))// \
4.53 + \ (_))" 9)
4.54 + Solve'_d2'_poly'_equation
4.55 + :: "[bool,real, \
4.56 + \ bool list] => bool list"
4.57 + ("((Script Solve'_d2'_poly'_equation (_ _ =))// \
4.58 + \ (_))" 9)
4.59 + Solve'_d2'_poly'_sqonly'_equation
4.60 + :: "[bool,real, \
4.61 + \ bool list] => bool list"
4.62 + ("((Script Solve'_d2'_poly'_sqonly'_equation (_ _ =))// \
4.63 + \ (_))" 9)
4.64 + Solve'_d2'_poly'_bdvonly'_equation
4.65 + :: "[bool,real, \
4.66 + \ bool list] => bool list"
4.67 + ("((Script Solve'_d2'_poly'_bdvonly'_equation (_ _ =))// \
4.68 + \ (_))" 9)
4.69 + Solve'_d2'_poly'_pq'_equation
4.70 + :: "[bool,real, \
4.71 + \ bool list] => bool list"
4.72 + ("((Script Solve'_d2'_poly'_pq'_equation (_ _ =))// \
4.73 + \ (_))" 9)
4.74 + Solve'_d2'_poly'_abc'_equation
4.75 + :: "[bool,real, \
4.76 + \ bool list] => bool list"
4.77 + ("((Script Solve'_d2'_poly'_abc'_equation (_ _ =))// \
4.78 + \ (_))" 9)
4.79 + Solve'_d3'_poly'_equation
4.80 + :: "[bool,real, \
4.81 + \ bool list] => bool list"
4.82 + ("((Script Solve'_d3'_poly'_equation (_ _ =))// \
4.83 + \ (_))" 9)
4.84 + Solve'_d4'_poly'_equation
4.85 + :: "[bool,real, \
4.86 + \ bool list] => bool list"
4.87 + ("((Script Solve'_d4'_poly'_equation (_ _ =))// \
4.88 + \ (_))" 9)
4.89 +
4.90 +(*-------------------- rules -------------------------------------------------*)
4.91 +rules
4.92 +
4.93 + cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \
4.94 + \ (a/c + b/c*bdv + bdv^^^2 = 0)"
4.95 + cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \
4.96 + \ (a/c - b/c*bdv + bdv^^^2 = 0)"
4.97 + cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \
4.98 + \ (a/c + b/c*bdv - bdv^^^2 = 0)"
4.99 +
4.100 + cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \
4.101 + \ (a/c + 1/c*bdv + bdv^^^2 = 0)"
4.102 + cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \
4.103 + \ (a/c - 1/c*bdv + bdv^^^2 = 0)"
4.104 + cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \
4.105 + \ (a/c + 1/c*bdv - bdv^^^2 = 0)"
4.106 +
4.107 + cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \
4.108 + \ ( b/c*bdv + bdv^^^2 = 0)"
4.109 + cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \
4.110 + \ ( b/c*bdv - bdv^^^2 = 0)"
4.111 +
4.112 + cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \
4.113 + \ ( 1/c*bdv + bdv^^^2 = 0)"
4.114 + cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \
4.115 + \ ( 1/c*bdv - bdv^^^2 = 0)"
4.116 +
4.117 + cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \
4.118 + \ (a/b + bdv^^^2 = 0)"
4.119 + cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \
4.120 + \ (a/b - bdv^^^2 = 0)"
4.121 + cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \
4.122 + \ ( bdv^^^2 = 0/b)"
4.123 +
4.124 + complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \
4.125 + \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
4.126 + complete_square2 "( p*bdv + bdv^^^2 = 0) = \
4.127 + \( (p/2 + bdv)^^^2 = (p/2)^^^2)"
4.128 + complete_square3 "( bdv + bdv^^^2 = 0) = \
4.129 + \( (1/2 + bdv)^^^2 = (1/2)^^^2)"
4.130 +
4.131 + complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \
4.132 + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
4.133 + complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \
4.134 + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
4.135 +
4.136 + square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
4.137 + square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
4.138 +
4.139 + bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
4.140 + bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
4.141 + bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)"
4.142 +
4.143 + plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
4.144 + minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*)
4.145 +
4.146 +(*-- normalize --*)
4.147 + all_left
4.148 + "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
4.149 + makex1_x
4.150 + "a^^^1 = a"
4.151 + real_assoc_1
4.152 + "a+(b+c) = a+b+c"
4.153 + real_assoc_2
4.154 + "a*(b*c) = a*b*c"
4.155 +
4.156 +(* ---- degree 0 ----*)
4.157 + d0_true
4.158 + "(0=0) = True"
4.159 + d0_false
4.160 + "[|Not(bdv occurs_in a);Not(a=!=0)|] ==> (a=0) = False"
4.161 +(* ---- degree 1 ----*)
4.162 + d1_isolate_add1
4.163 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = -a)"
4.164 + d1_isolate_add2
4.165 + "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = -a)"
4.166 + d1_isolate_div
4.167 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
4.168 +(* ---- degree 2 ----*)
4.169 + d2_isolate_add1
4.170 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= -a)"
4.171 + d2_isolate_add2
4.172 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= -a)"
4.173 + d2_isolate_div
4.174 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
4.175 + d2_prescind1
4.176 + "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
4.177 + d2_prescind2
4.178 + "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
4.179 + d2_prescind3
4.180 + "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
4.181 + d2_prescind4
4.182 + "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
4.183 + (* eliminate degree 2 *)
4.184 + d2_sqrt_equation1
4.185 + "[|(0<=c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=-sqrt c ))"
4.186 + d2_sqrt_equation2
4.187 + "(bdv^^^2=0) = (bdv=0)"
4.188 + d2_sqrt_equation3
4.189 + "(b*bdv^^^2=0) = (bdv=0)"
4.190 + d2_reduce_equation1
4.191 + "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
4.192 + d2_reduce_equation2
4.193 + "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
4.194 + d2_pqformula1
4.195 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
4.196 + ((bdv= -(p/2) + sqrt(p^^^2 - 4*q)/2)
4.197 + | (bdv= -(p/2) - sqrt(p^^^2 - 4*q)/2))"
4.198 + d2_pqformula2
4.199 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
4.200 + ((bdv= -(p/2) + sqrt(p^^^2 - 4*q)/2)
4.201 + | (bdv= -(p/2) - sqrt(p^^^2 - 4*q)/2))"
4.202 + d2_pqformula3
4.203 + "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
4.204 + ((bdv= -(1/2) + sqrt(1 - 4*q)/2)
4.205 + | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"
4.206 + d2_pqformula4
4.207 + "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
4.208 + ((bdv= -(1/2) + sqrt(1 - 4*q)/2)
4.209 + | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"
4.210 + d2_pqformula5
4.211 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
4.212 + ((bdv= -(p/2) + sqrt(p^^^2 - 0)/2)
4.213 + | (bdv= -(p/2) - sqrt(p^^^2 - 0)/2))"
4.214 + d2_pqformula6
4.215 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
4.216 + ((bdv= -(p/2) + sqrt(p^^^2 - 0)/2)
4.217 + | (bdv= -(p/2) - sqrt(p^^^2 - 0)/2))"
4.218 + d2_pqformula7
4.219 + "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
4.220 + ((bdv= -(1/2) + sqrt(1 - 0)/2)
4.221 + | (bdv= -(1/2) - sqrt(1 - 0)/2))"
4.222 + d2_pqformula8
4.223 + "[|0<=1 - 4*q|] ==> ( bdv+1*bdv^^^2=0) =
4.224 + ((bdv= -(1/2) + sqrt(1 - 4*q)/2)
4.225 + | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"
4.226 + d2_pqformula9
4.227 + "[|0<= - 4*q|] ==> (q+ 1*bdv^^^2=0) =
4.228 + ((bdv= 0 + sqrt(0 - 4*q)/2)
4.229 + | (bdv= 0 - sqrt(0 - 4*q)/2))"
4.230 + d2_pqformula10
4.231 + "[|0<= - 4*q|] ==> (q+ bdv^^^2=0) =
4.232 + ((bdv= 0 + sqrt(0 - 4*q)/2)
4.233 + | (bdv= 0 - sqrt(0 - 4*q)/2))"
4.234 + d2_abcformula1
4.235 + "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
4.236 + ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
4.237 + | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
4.238 + d2_abcformula2
4.239 + "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
4.240 + ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
4.241 + | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
4.242 + d2_abcformula3
4.243 + "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+ bdv^^^2=0) =
4.244 + ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
4.245 + | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
4.246 + d2_abcformula4
4.247 + "[|0<=b^^^2 - 4*a*c|] ==> (c + bdv+ bdv^^^2=0) =
4.248 + ((bdv=( -b + sqrt(1 - 4*1*c))/(2*1))
4.249 + | (bdv=( -b - sqrt(1 - 4*1*c))/(2*1)))"
4.250 + d2_abcformula5
4.251 + "[|0<=b^^^2 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
4.252 + ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
4.253 + | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
4.254 + d2_abcformula6
4.255 + "[|0<=1 - 4*a*c|] ==> (c+ bdv^^^2=0) =
4.256 + ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
4.257 + | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
4.258 + d2_abcformula7
4.259 + "[|0<=1 - 4*a*c|] ==> ( b*bdv+a*bdv^^^2=0) =
4.260 + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
4.261 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
4.262 + d2_abcformula8
4.263 + "[|0<=b^^^2 - 4*a*c|] ==> ( b*bdv+ bdv^^^2=0) =
4.264 + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
4.265 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
4.266 + d2_abcformula9
4.267 + "[|0<=1 - 4*a*c|] ==> ( bdv+a*bdv^^^2=0) =
4.268 + ((bdv=( -1 + sqrt(1 - 0))/(2*a))
4.269 + | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
4.270 + d2_abcformula10
4.271 + "[|0<=b^^^2 - 4*a*c|] ==> ( bdv+ bdv^^^2=0) =
4.272 + ((bdv=( -1 + sqrt(1 - 0))/(2*1))
4.273 + | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
4.274 +(* ---- degree 3 ----*)
4.275 + d3_reduce_equation1
4.276 + "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
4.277 + d3_reduce_equation2
4.278 + "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
4.279 + d3_reduce_equation3
4.280 + "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
4.281 + d3_reduce_equation4
4.282 + "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
4.283 + d3_reduce_equation5
4.284 + "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
4.285 + d3_reduce_equation6
4.286 + "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
4.287 + d3_reduce_equation7
4.288 + "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
4.289 + d3_reduce_equation8
4.290 + "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
4.291 + d3_reduce_equation9
4.292 + "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
4.293 + d3_reduce_equation10
4.294 + "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
4.295 + d3_reduce_equation11
4.296 + "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
4.297 + d3_reduce_equation12
4.298 + "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
4.299 + d3_reduce_equation13
4.300 + "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
4.301 + d3_reduce_equation14
4.302 + "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
4.303 + d3_reduce_equation15
4.304 + "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
4.305 + d3_reduce_equation16
4.306 + "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
4.307 + d3_isolate_add1
4.308 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
4.309 + d3_isolate_add2
4.310 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
4.311 + d3_isolate_div
4.312 + "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
4.313 + d3_root_equation2
4.314 + "(bdv^^^3=0) = (bdv=0)"
4.315 + d3_root_equation1
4.316 + "(bdv^^^3=c) = (bdv = nroot 3 c)"
4.317 +
4.318 +(* ---- degree 4 ----*)
4.319 + (* FIXME es wir nicht getestet ob u>0 *)
4.320 + d4_sub_u1
4.321 + "(c+b*bdv^^^2+a*bdv^^^4=0) =
4.322 + ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
4.323 +
4.324 +(* ---- 7.3.02 von Termorder ---- *)
4.325 +
4.326 + bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
4.327 + bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
4.328 + bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
4.329 +
4.330 +(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
4.331 + bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
4.332 + bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
4.333 +*)
4.334 + bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
4.335 + bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
4.336 + bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
4.337 +
4.338 + bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
4.339 + bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
4.340 + bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
4.341 +
4.342 +
4.343 + bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
4.344 + bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
4.345 + bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
4.346 +
4.347 + bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
4.348 + bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
4.349 + bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
4.350 +
4.351 + bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
4.352 + bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
4.353 + bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
4.354 +
4.355 +(*WN.14.3.03*)
4.356 + real_minus_div "- (a / b) = (-1 * a) / b"
4.357 +
4.358 + separate_bdv "(a * bdv) / b = (a / b) * bdv"
4.359 + separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
4.360 + separate_1_bdv "bdv / b = (1 / b) * bdv"
4.361 + separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
4.362 +
4.363 +end
4.364 +
4.365 +
4.366 +
4.367 +
4.368 +
4.369 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/IsacKnowledge/RatEq.ML Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,170 @@
5.4 +(* (c) by Richard Lang
5.5 + collecting all knowledge for RationalEquations
5.6 + created by: rlang
5.7 + date: 02.09
5.8 + changed by: rlang
5.9 + last change by: rlang
5.10 + date: 02.11.29
5.11 +*)
5.12 +
5.13 +(* use"knowledge/RatEq.ML";
5.14 + use"RatEq.ML";
5.15 + remove_thy"RatEq";
5.16 + use_thy"Isac";
5.17 +
5.18 + use"ROOT.ML";
5.19 + cd"knowledge";
5.20 + *)
5.21 +"******* RatEq.ML begin *******";
5.22 +
5.23 +theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]);
5.24 +
5.25 +(*-------------------------functions-----------------------*)
5.26 +(* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
5.27 +fun is_rateqation_in t v =
5.28 + let
5.29 + fun coeff_in c v = v mem (vars c);
5.30 + fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
5.31 + (* at the moment there is no term like this, but ....*)
5.32 + | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
5.33 + | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) orelse (finddivide t2 v)
5.34 + | finddivide (_ $ t1) v = (finddivide t1 v)
5.35 + | finddivide _ _ = false;
5.36 + in
5.37 + finddivide t v
5.38 + end;
5.39 +
5.40 +fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
5.41 + if is_rateqation_in t v then
5.42 + Some ((term2str p) ^ " = True",
5.43 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
5.44 + else Some ((term2str p) ^ " = True",
5.45 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
5.46 + | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);
5.47 +
5.48 +(*-------------------------rulse-----------------------*)
5.49 +val rateq_prls = (*15.10.02:just the following order due to subterm evaluation*)
5.50 + append_rls "rateq_prls" e_rls
5.51 + [Calc ("Atools.ident",eval_ident "#ident_"),
5.52 + Calc ("Tools.matches",eval_matches ""),
5.53 + Calc ("Tools.lhs" ,eval_lhs ""),
5.54 + Calc ("Tools.rhs" ,eval_rhs ""),
5.55 + Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
5.56 + Calc ("op =",eval_equal "#equal_"),
5.57 + Thm ("not_true",num_str not_true),
5.58 + Thm ("not_false",num_str not_false),
5.59 + Thm ("and_true",num_str and_true),
5.60 + Thm ("and_false",num_str and_false),
5.61 + Thm ("or_true",num_str or_true),
5.62 + Thm ("or_false",num_str or_false),
5.63 + Thm ("and_commute",num_str and_commute),
5.64 + Thm ("or_commute",num_str or_commute)
5.65 + ];
5.66 +
5.67 +(*rls = merge_rls erls poly_erls *)
5.68 + remove_rls "no_commute" (*ein Hack*)
5.69 + remove_rls "rateq_erls" (*WN: ein Hack*)
5.70 + (merge_rls "is_ratequation_in" calculate_Rational
5.71 + (append_rls "is_ratequation_in"
5.72 + poly_erls
5.73 + [(*Calc ("HOL.divide", eval_cancel "#divide_"),*)
5.74 + Calc ("RatEq.is'_ratequation'_in",
5.75 + eval_is_ratequation_in "")
5.76 + [Thm ("and_commute",num_str and_commute), (*ein Hack*)
5.77 + Thm ("or_commute",num_str or_commute) (*ein Hack*)
5.78 + Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
5.79 + ];
5.80 +ruleset' := overwritel (!ruleset',
5.81 + [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
5.82 + ]);
5.83 +
5.84 +val rat_eliminate =
5.85 + erls = rateq_erls, srls = Erls, calc = [], asm_thm = [],
5.86 + ("rat_mult_denominator_right","")],
5.87 + rules = [
5.88 + Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),
5.89 + (* a/b=c/d -> ad=cb *)
5.90 + Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),
5.91 + (* a =c/d -> ad=c *)
5.92 + Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)
5.93 + (* a/b=c -> a=cb *)
5.94 + ],
5.95 + scr = Script ((term_of o the o (parse thy)) "empty_script")
5.96 + }:rls;
5.97 +ruleset' := overwritel (!ruleset',
5.98 + [("rat_eliminate",rat_eliminate)
5.99 + ]);
5.100 +
5.101 +
5.102 +
5.103 +val rat_simplify =
5.104 + erls = rateq_erls, srls = Erls, calc = [], asm_thm = [],
5.105 + ("rat_double_rat_3","")],
5.106 + rules = [
5.107 + Thm("real_rat_mult_1",num_str real_rat_mult_1),
5.108 + (*a*(b/c) = (a*b)/c*)
5.109 + Thm("real_rat_mult_2",num_str real_rat_mult_2),
5.110 + (*(a/b)*(c/d) = (a*c)/(b*d)*)
5.111 + Thm("real_rat_mult_3",num_str real_rat_mult_3),
5.112 + (* (a/b)*c = (a*c)/b*)
5.113 + Thm("real_rat_pow",num_str real_rat_pow),
5.114 + (*(a/b)^^^2 = a^^^2/b^^^2*)
5.115 + Thm("real_diff_minus",num_str real_diff_minus),
5.116 + (* a - b = a + (-1) * b *)
5.117 + Thm("rat_double_rat_1",num_str rat_double_rat_1),
5.118 + (* (a / (c/d) = (a*d) / c) *)
5.119 + Thm("rat_double_rat_2",num_str rat_double_rat_2),
5.120 + (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
5.121 + Thm("rat_double_rat_3",num_str rat_double_rat_3)
5.122 + (* ((a/b) / c = a / (b*c) ) *)
5.123 + ],
5.124 + scr = Script ((term_of o the o (parse thy)) "empty_script")
5.125 + }:rls;
5.126 +ruleset' := overwritel (!ruleset',
5.127 + [("rat_simplify",rat_simplify)
5.128 + ]);
5.129 +
5.130 +(*-------------------------Problem-----------------------*)
5.131 +(*
5.132 +(get_pbt ["rational","univariate","equation"]);
5.133 +show_ptyps();
5.134 +*)
5.135 +store_pbt
5.136 + (prep_pbt RatEq.thy
5.137 + (["rational","univariate","equation"],
5.138 + [("#Given" ,["equality e_","solveFor v_"]),
5.139 + ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
5.140 + ("#Find" ,["solutions v_i_"])
5.141 + ],
5.142 + [("RatEq.thy","solve_rat_equation")]));
5.143 + [["RatEq","solve_rat_equation"]]));
5.144 +
5.145 +methods:= overwritel (!methods,
5.146 +[
5.147 + prep_met
5.148 + (("RatEq.thy","solve_rat_equation"),
5.149 + (["RatEq","solve_rat_equation"],
5.150 + [("#Given" ,["equality e_","solveFor v_"]),
5.151 + ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
5.152 + ("#Find" ,["solutions v_i_"])
5.153 + ],
5.154 + {rew_ord'="termlessI",
5.155 + rls'=rateq_erls,
5.156 + srls=e_rls,
5.157 + prls=rateq_prls,
5.158 + asm_rls=["rat_simplify","rat_eliminate"],
5.159 + asm_rls=[],
5.160 + asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""),
5.161 + ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
5.162 + ("rat_mult_denominator_right","")]},
5.163 + "Script Solve_rat_equation (e_::bool) (v_::real) = \
5.164 + \(let e_ = ((Repeat(Try (Rewrite_Set rat_simplify True))) @@ \
5.165 + \ (Repeat(Try (Rewrite_Set make_polynomial False))) @@ \
5.166 + \ (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ \
5.167 + \ (Repeat(Try (Rewrite_Set rat_eliminate True)))) e_;\
5.168 + \ (RatEq_,no_met)) [bool_ e_, real_ v_]) \
5.169 + \ [no_met]) [bool_ e_, real_ v_]) \
5.170 + )
5.171 +]);
5.172 + ));
5.173 +"******* RatEq.ML end *******";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/IsacKnowledge/RatEq.thy Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,67 @@
6.4 +(* (c) by Richard Lang
6.5 + theory collecting all knowledge for RationalEquations
6.6 + created by: rlang
6.7 + date: 02.08.12
6.8 + changed by: rlang
6.9 + last change by: rlang
6.10 + date: 02.11.28
6.11 +*)
6.12 +
6.13 +(*
6.14 + RL.020812
6.15 + use_thy"knowledge/RatEq";
6.16 + use_thy"RatEq";
6.17 + use_thy_only"RatEq";
6.18 +
6.19 + remove_thy"RatEq";
6.20 + use_thy"Isac";
6.21 +
6.22 + use"ROOT.ML";
6.23 + cd"knowledge";
6.24 + *)
6.25 +RatEq = Rational +
6.26 +
6.27 +(*-------------------- consts------------------------------------------------*)
6.28 +consts
6.29 +
6.30 + is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
6.31 +
6.32 + (*----------------------scripts-----------------------*)
6.33 + Solve'_rat'_equation
6.34 + :: "[bool,real, \
6.35 + \ bool list] => bool list"
6.36 + ("((Script Solve'_rat'_equation (_ _ =))// \
6.37 + \ (_))" 9)
6.38 +
6.39 +(*-------------------- rules------------------------------------------------*)
6.40 +rules
6.41 + (* FIXME also in Poly.thy def. --> FIXED*)
6.42 + (*real_diff_minus
6.43 + "a - b = a + (-1) * b"*)
6.44 + real_rat_mult_1
6.45 + "a*(b/c) = (a*b)/c"
6.46 + real_rat_mult_2
6.47 + "(a/b)*(c/d) = (a*c)/(b*d)"
6.48 + real_rat_mult_3
6.49 + "(a/b)*c = (a*c)/b"
6.50 + real_rat_pow
6.51 + "(a/b)^^^2 = a^^^2/b^^^2"
6.52 +
6.53 + rat_double_rat_1
6.54 + "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
6.55 + rat_double_rat_2
6.56 + "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"
6.57 + rat_double_rat_3
6.58 + "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
6.59 +
6.60 +
6.61 + (* equation to same denominator *)
6.62 + rat_mult_denominator_both
6.63 + "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
6.64 + rat_mult_denominator_left
6.65 + "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
6.66 + rat_mult_denominator_right
6.67 + "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
6.68 +
6.69 +
6.70 +end