1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 02 15:27:47 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 02 15:30:41 2021 +0200
1.3 @@ -322,7 +322,6 @@
1.4
1.5 (** )end;( *local*)
1.6
1.7 -\<close> ML \<open>
1.8 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.9 if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
1.10
2.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 02 15:27:47 2021 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 02 15:30:41 2021 +0200
2.3 @@ -108,1176 +108,6 @@
2.4 \<close> ML \<open>
2.5 \<close>
2.6
2.7 -(** )ML_file \<open>Knowledge/polyeq-1.sml\<close>( **)
2.8 -section \<open>======== check Knowledge/polyeq-1.sml =============================================\<close>
2.9 -ML \<open>
2.10 -\<close> text \<open> =======-------------------------vvv polyeq-1.sml-------TOODOO----------------
2.11 -\<close> ML \<open>
2.12 -(* Title: Knowledge/polyeq-1.sml
2.13 - testexamples for PolyEq, poynomial equations and equational systems
2.14 - Author: Richard Lang 2003
2.15 - (c) due to copyright terms
2.16 -WN030609: some expls dont work due to unfinished handling of 'expanded terms';
2.17 - others marked with TODO have to be checked, too.
2.18 -*)
2.19 -
2.20 -"-----------------------------------------------------------------";
2.21 -"table of contents -----------------------------------------------";
2.22 -"-----------------------------------------------------------------";
2.23 -"------ polyeq- 1.sml ---------------------------------------------";
2.24 -"----------- tests on predicates in problems ---------------------";
2.25 -"----------- test matching problems ------------------------------";
2.26 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
2.27 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
2.28 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
2.29 -"----------- lin.eq degree_0 -------------------------------------";
2.30 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
2.31 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
2.32 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
2.33 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
2.34 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
2.35 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
2.36 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
2.37 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
2.38 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
2.39 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
2.40 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
2.41 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
2.42 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
2.43 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
2.44 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
2.45 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
2.46 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.47 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
2.48 -"-----------------------------------------------------------------";
2.49 -"------ polyeq- 2.sml ---------------------------------------------";
2.50 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
2.51 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.52 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
2.53 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
2.54 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
2.55 -"----------- rls make_polynomial_in ------------------------------";
2.56 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
2.57 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
2.58 -"-----------------------------------------------------------------";
2.59 -"-----------------------------------------------------------------";
2.60 -
2.61 -\<close> ML \<open>
2.62 -"----------- tests on predicates in problems ---------------------";
2.63 -"----------- tests on predicates in problems ---------------------";
2.64 -"----------- tests on predicates in problems ---------------------";
2.65 -Rewrite.trace_on:=false; (*true false*)
2.66 -
2.67 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
2.68 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
2.69 - if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
2.70 - else error "polyeq.sml: diff.behav. in lhs";
2.71 -
2.72 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
2.73 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
2.74 - if (UnparseC.term t) = "True" then ()
2.75 - else error "polyeq.sml: diff.behav. 1 in is_expended_in";
2.76 -
2.77 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
2.78 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
2.79 - if (UnparseC.term t) = "False" then ()
2.80 - else error "polyeq.sml: diff.behav. 2 in is_poly_in";
2.81 -
2.82 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
2.83 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
2.84 - if (UnparseC.term t) = "True" then ()
2.85 - else error "polyeq.sml: diff.behav. 3 in is_poly_in";
2.86 -
2.87 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
2.88 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
2.89 - if (UnparseC.term t) = "True" then ()
2.90 - else error "polyeq.sml: diff.behav. 4 in is_expended_in";
2.91 -
2.92 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
2.93 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
2.94 - if (UnparseC.term t) = "True" then ()
2.95 - else error "polyeq.sml: diff.behav. 5 in is_expended_in";
2.96 -
2.97 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
2.98 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
2.99 - if (UnparseC.term t) = "True" then ()
2.100 - else error "polyeq.sml: diff.behav. in has_degree_in_in";
2.101 -
2.102 -\<close> ML \<open> (*TOODOO broken with repair ord_make_polynomial_in*)
2.103 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
2.104 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
2.105 - if (UnparseC.term t) = "False" then ()
2.106 - else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
2.107 -
2.108 -\<close> ML \<open>
2.109 - val t4 = (Thm.term_of o the o (TermC.parse thy))
2.110 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
2.111 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
2.112 - if (UnparseC.term t) = "False" then ()
2.113 - else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
2.114 -
2.115 -val t5 = (Thm.term_of o the o (TermC.parse thy))
2.116 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
2.117 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
2.118 - if (UnparseC.term t) = "True" then ()
2.119 - else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
2.120 -
2.121 -\<close> ML \<open> (* M_Match.match_pbl [expanded,univariate,equation] *)
2.122 -"----------- test matching problems --------------------------0---";
2.123 -"----------- test matching problems --------------------------0---";
2.124 -"----------- test matching problems --------------------------0---";
2.125 -val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.126 -if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
2.127 - M_Match.Matches' {Find = [Correct "solutions L"],
2.128 - With = [],
2.129 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
2.130 - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
2.131 - Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
2.132 - Relate = []}
2.133 -then () else error "M_Match.match_pbl [expanded,univariate,equation]";
2.134 -
2.135 -\<close> ML \<open>
2.136 -if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
2.137 - M_Match.Matches' {Find = [Correct "solutions L"],
2.138 - With = [],
2.139 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
2.140 - Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
2.141 - Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
2.142 -then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
2.143 -
2.144 -\<close> ML \<open>
2.145 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
2.146 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
2.147 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
2.148 -(*##################################################################################
2.149 ------------ 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
2.150 -
2.151 - (*Aufgabe zum Einstieg in die Arbeit...*)
2.152 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
2.153 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
2.154 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
2.155 - UnparseC.term t;
2.156 - "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
2.157 - val SOME (t,_) =
2.158 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
2.159 - UnparseC.term t;
2.160 - "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
2.161 -(* bei Verwendung von "size_of-term" nach MG :*)
2.162 -(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
2.163 -
2.164 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
2.165 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
2.166 - UnparseC.term t;
2.167 - "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
2.168 -(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
2.169 -
2.170 - val SOME (t,_) =
2.171 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
2.172 - UnparseC.term t;
2.173 - "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
2.174 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
2.175 - "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
2.176 -
2.177 - (*das rewriting l"asst sich beobachten mit
2.178 -Rewrite.trace_on := false; (*true false*)
2.179 - *)
2.180 -
2.181 -"------ 15.11.02 --------------------------";
2.182 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
2.183 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
2.184 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
2.185 -
2.186 -Rewrite.trace_on := false; (*true false*)
2.187 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
2.188 - val SOME (t,_) =
2.189 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.190 - UnparseC.term t;
2.191 - val SOME (t,_) =
2.192 - rewrite_set_ thy false discard_parentheses t;
2.193 - UnparseC.term t;
2.194 -"1 + b * x + x * a";
2.195 -
2.196 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
2.197 - val SOME (t,_) =
2.198 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.199 - UnparseC.term t;
2.200 - val SOME (t,_) =
2.201 - rewrite_set_ thy false discard_parentheses t;
2.202 - UnparseC.term t;
2.203 -"1 + (x + b * x) * a + a \<up> 2";
2.204 -
2.205 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
2.206 - val SOME (t,_) =
2.207 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.208 - UnparseC.term t;
2.209 - val SOME (t,_) =
2.210 - rewrite_set_ thy false discard_parentheses t;
2.211 - UnparseC.term t;
2.212 -"1 + b * a + (7 + x) * a \<up> 2";
2.213 -
2.214 -(* MG2003
2.215 - Prog_Expr.thy grundlegende Algebra
2.216 - Poly.thy Polynome
2.217 - Rational.thy Br"uche
2.218 - Root.thy Wurzeln
2.219 - RootRat.thy Wurzen + Br"uche
2.220 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
2.221 -
2.222 - get_thm Termorder.thy "bdv_n_collect";
2.223 - get_thm (theory "Isac_Knowledge") "bdv_n_collect";
2.224 -*)
2.225 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
2.226 - val SOME (t,_) =
2.227 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.228 - UnparseC.term t;
2.229 - val SOME (t,_) =
2.230 - rewrite_set_ thy false discard_parentheses t;
2.231 - UnparseC.term t;
2.232 -"(7 + x) * a \<up> 2";
2.233 -
2.234 - val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
2.235 -
2.236 - val t = (Thm.term_of o the o (parseold thy)) "7";
2.237 -##################################################################################*)
2.238 -
2.239 -
2.240 -\<close> ML \<open>
2.241 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
2.242 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
2.243 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
2.244 -(* termorder hacked by MG, adapted later by WN *)
2.245 -(** )local ( *. for make_polynomial_in .*)
2.246 -
2.247 -open Term; (* for type order = EQUAL | LESS | GREATER *)
2.248 -
2.249 -fun pr_ord EQUAL = "EQUAL"
2.250 - | pr_ord LESS = "LESS"
2.251 - | pr_ord GREATER = "GREATER";
2.252 -
2.253 -fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
2.254 - | dest_hd' x (t as Free (a, T)) =
2.255 - if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
2.256 - else (((a, 0), T), 1)
2.257 - | dest_hd' _ (Var v) = (v, 2)
2.258 - | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
2.259 - | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
2.260 - | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
2.261 -
2.262 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
2.263 - Free (var, _) $ Free (pot, _)) =
2.264 - (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
2.265 - case x of (*WN*)
2.266 - (Free (xstr, _)) =>
2.267 - if xstr = var
2.268 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
2.269 - 1000 * (the (TermC.int_opt_of_string pot)))
2.270 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
2.271 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
2.272 - | size_of_term' i pr x (t as Abs (_, _, body)) =
2.273 - (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
2.274 - 1 + size_of_term' (i + 1) pr x body)
2.275 - | size_of_term' i pr x (f $ t) =
2.276 - let
2.277 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
2.278 - val s1 = size_of_term' (i + 1) pr x f
2.279 - val s2 = size_of_term' (i + 1) pr x t
2.280 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
2.281 - in (s1 + s2) end
2.282 - | size_of_term' i pr x t =
2.283 - (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
2.284 - case t of
2.285 - Free (subst, _) =>
2.286 - (case x of
2.287 - Free (xstr, _) =>
2.288 - if xstr = subst
2.289 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
2.290 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
2.291 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
2.292 - | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
2.293 -
2.294 -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.295 - let
2.296 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
2.297 - val ord =
2.298 - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
2.299 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
2.300 - in ord end
2.301 - | term_ord' i pr x _ (t, u) =
2.302 - let
2.303 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
2.304 - val ord =
2.305 - case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
2.306 - EQUAL =>
2.307 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u
2.308 - in
2.309 - (case hd_ord (i + 1) pr x (f, g) of
2.310 - EQUAL => (terms_ord x (i + 1) pr) (ts, us)
2.311 - | ord => ord)
2.312 - end
2.313 - | ord => ord
2.314 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
2.315 - in ord end
2.316 -and hd_ord i pr x (f, g) = (* ~ term.ML *)
2.317 - let
2.318 - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
2.319 - val ord = prod_ord
2.320 - (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
2.321 - (dest_hd' x f, dest_hd' x g)
2.322 - val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
2.323 - in ord end
2.324 -and terms_ord x i pr (ts, us) =
2.325 - let
2.326 - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
2.327 - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
2.328 - val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
2.329 - in ord end
2.330 -
2.331 -(** )in( *local*)
2.332 -
2.333 -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
2.334 - ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
2.335 - case subst of
2.336 - (_, x) :: _ =>
2.337 - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
2.338 - | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
2.339 -
2.340 -(** )end;( *local*)
2.341 -
2.342 -\<close> ML \<open>
2.343 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
2.344 -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
2.345 -
2.346 -val x = TermC.str2term "x ::real";
2.347 -
2.348 -\<close> ML \<open>
2.349 -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
2.350 -if 2006 = size_of_term' 1 true x t1
2.351 -then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
2.352 -
2.353 -\<close> ML \<open>
2.354 -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
2.355 -if 3004 = size_of_term' 1 true x t2
2.356 -then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
2.357 -
2.358 -
2.359 -\<close> ML \<open>
2.360 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
2.361 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
2.362 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
2.363 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
2.364 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
2.365 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
2.366 -
2.367 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
2.368 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
2.369 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
2.370 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
2.371 -
2.372 -\<close> ML \<open>
2.373 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
2.374 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
2.375 -
2.376 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
2.377 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
2.378 -
2.379 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
2.380 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
2.381 -
2.382 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
2.383 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
2.384 - ord_make_polynomial_in true thy substx (aa, bb);
2.385 - true; (* => LESS *)
2.386 -
2.387 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
2.388 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
2.389 - ord_make_polynomial_in true thy substa (aa, bb);
2.390 - false; (* => GREATER *)
2.391 -
2.392 -\<close> ML \<open>
2.393 -(* und nach dem Re-engineering der Termorders in den 'rulesets'
2.394 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
2.395 - val bdv= TermC.str2term "bdv ::real";
2.396 - val x = TermC.str2term "x ::real";
2.397 - val a = TermC.str2term "a ::real";
2.398 - val b = TermC.str2term "b ::real";
2.399 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
2.400 -if UnparseC.term t' = "b + x + a" then ()
2.401 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
2.402 -
2.403 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
2.404 -
2.405 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
2.406 -if UnparseC.term t' = "a + b + x" then ()
2.407 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
2.408 -
2.409 -\<close> ML \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
2.410 - val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
2.411 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
2.412 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
2.413 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
2.414 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
2.415 -
2.416 -\<close> ML \<open>
2.417 - val ttt' = "(3*x + 5)/18 ::real";
2.418 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
2.419 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
2.420 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
2.421 -else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
2.422 -
2.423 -\<close> ML \<open>
2.424 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
2.425 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
2.426 -else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
2.427 -
2.428 -\<close> ML \<open>
2.429 -"----------- lin.eq degree_0 -------------------------------------";
2.430 -"----------- lin.eq degree_0 -------------------------------------";
2.431 -"----------- lin.eq degree_0 -------------------------------------";
2.432 -"----- d0_false ------";
2.433 -val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
2.434 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
2.435 - ["PolyEq", "solve_d0_polyeq_equation"]);
2.436 -(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
2.437 -TODO: change to "equality (x + - 1*x = (0::real))"
2.438 - and search for an appropriate problem and method.
2.439 -
2.440 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.441 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.442 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.443 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.444 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.445 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.446 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.447 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
2.448 - | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
2.449 -
2.450 -"----- d0_true ------";
2.451 -val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
2.452 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
2.453 - ["PolyEq", "solve_d0_polyeq_equation"]);
2.454 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.455 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.456 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.457 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.458 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.459 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.460 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.461 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
2.462 - | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
2.463 -============ inhibit exn WN110914 ============================================*)
2.464 -
2.465 -\<close> text \<open>
2.466 -(*rewrite_set_, rewrite_ "- 1 / 4 = - 1 / 4" z =
2.467 -- 1 * (- 1 / 4 / 2) + sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2 \<or>
2.468 -z =
2.469 -- 1 * (- 1 / 4 / 2) + - 1 * (sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2) = NONE*)
2.470 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
2.471 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
2.472 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
2.473 -"----- d2_pqformula1 ------!!!!";
2.474 -val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
2.475 -val (dI',pI',mI') =
2.476 - ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
2.477 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.478 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.479 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.480 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.481 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.482 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.483 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.484 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
2.485 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.486 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.487 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.488 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.489 -
2.490 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
2.491 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
2.492 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.493 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.494 -
2.495 -if p = ([], Res) andalso
2.496 - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
2.497 - case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
2.498 -else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
2.499 -
2.500 -\<close> ML \<open>
2.501 -Rewrite.trace_on := false; (*true false*)
2.502 -\<close> ML \<open>
2.503 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
2.504 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
2.505 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
2.506 -"----- d2_pqformula1_neg ------";
2.507 -val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
2.508 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.509 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.510 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.511 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.512 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.513 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.514 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.515 -(*### or2list False
2.516 - ([1],Res) False Or_to_List)*)
2.517 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.518 -(*### or2list False
2.519 - ([2],Res) [] Check_elementwise "Assumptions"*)
2.520 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.521 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.522 -val asm = Ctree.get_assumptions pt p;
2.523 -if f2str f = "[]" andalso
2.524 - UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
2.525 - "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
2.526 -else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
2.527 -
2.528 -\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
2.529 -x = - 1 * (- 1 / 2) + - 1 * (sqrt ((- 1) \<up> 2 + 8) / 2) = NONE*)
2.530 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
2.531 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
2.532 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
2.533 -"----- d2_pqformula2 ------";
2.534 -val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.535 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.536 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.537 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.538 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.539 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.540 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.541 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.542 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.543 -
2.544 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.545 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.546 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.547 -case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
2.548 - | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
2.549 -
2.550 -
2.551 -\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
2.552 -exception TYPE raised (line 169 of "consts.ML"): Illegal type for constant "HOL.eq" :: real
2.553 - \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool*)
2.554 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
2.555 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
2.556 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
2.557 -"----- d2_pqformula3 ------";
2.558 -(*EP-9*)
2.559 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.560 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.561 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.562 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.563 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.564 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.565 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.566 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.567 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.568 -
2.569 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.570 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.571 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.572 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
2.573 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
2.574 -
2.575 -
2.576 -\<close> ML \<open>
2.577 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
2.578 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
2.579 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
2.580 -"----- d2_pqformula3_neg ------";
2.581 -val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.582 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.583 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.584 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.585 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.586 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.587 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.588 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.589 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.590 -
2.591 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.592 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.593 -"TODO 2 + x + x \<up> 2 = 0";
2.594 -"TODO 2 + x + x \<up> 2 = 0";
2.595 -"TODO 2 + x + x \<up> 2 = 0";
2.596 -
2.597 -\<close> text \<open> (*see TOODOO.1*)
2.598 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
2.599 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
2.600 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
2.601 -"----- d2_pqformula4 ------";
2.602 -val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.603 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.604 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.605 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.606 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.607 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.608 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.609 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.610 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.611 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.612 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.613 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.614 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
2.615 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
2.616 -
2.617 -\<close> text \<open> (* FormKF "[]" instead of "[x = 0, x = - 1]"*)
2.618 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
2.619 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
2.620 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
2.621 -"----- d2_pqformula5 ------";
2.622 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.623 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.624 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.625 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.626 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.627 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.628 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.629 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.630 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.631 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.632 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.633 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.634 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.635 - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
2.636 -
2.637 -\<close> text \<open> (* TOODOO.1 *)
2.638 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
2.639 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
2.640 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
2.641 -"----- d2_pqformula6 ------";
2.642 -val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.643 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.644 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.645 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.646 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.647 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.648 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.649 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.650 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.651 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.652 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.653 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.654 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.655 - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
2.656 -
2.657 -\<close> text \<open> (* TOODOO.1*)
2.658 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
2.659 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
2.660 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
2.661 -"----- d2_pqformula7 ------";
2.662 -(*EP- 10*)
2.663 -val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.664 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.665 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.666 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.667 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.668 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.669 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.670 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.671 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.672 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.673 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.674 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.675 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.676 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
2.677 -
2.678 -\<close> text \<open> (* TOODOO.1*)
2.679 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
2.680 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
2.681 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
2.682 -"----- d2_pqformula8 ------";
2.683 -val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.684 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.685 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.686 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.687 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.688 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.689 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.690 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.691 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.692 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.693 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.694 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.695 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.696 - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
2.697 -
2.698 -\<close> text \<open> (* TOODOO.1*)
2.699 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
2.700 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
2.701 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
2.702 -"----- d2_pqformula9 ------";
2.703 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.704 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.705 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.706 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.707 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.708 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.709 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.710 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.711 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.712 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.713 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.714 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
2.715 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
2.716 -
2.717 -
2.718 -\<close> ML \<open>
2.719 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
2.720 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
2.721 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
2.722 -"----- d2_pqformula9_neg ------";
2.723 -val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.724 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
2.725 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
2.726 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.727 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.728 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.729 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.730 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.731 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.732 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.733 -"TODO 4 + 1*x \<up> 2 = 0";
2.734 -"TODO 4 + 1*x \<up> 2 = 0";
2.735 -"TODO 4 + 1*x \<up> 2 = 0";
2.736 -
2.737 -\<close> text \<open> (*see TOODOO.1*)
2.738 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
2.739 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
2.740 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
2.741 -val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.742 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.743 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.744 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.745 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.746 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.747 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.748 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.749 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.750 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.751 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.752 -case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
2.753 - | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
2.754 -
2.755 -\<close> ML \<open>
2.756 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
2.757 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
2.758 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
2.759 -val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.760 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.761 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.762 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.763 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.764 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.765 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.766 -
2.767 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.768 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.769 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.770 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
2.771 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
2.772 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
2.773 -
2.774 -
2.775 -\<close> text \<open> (*see TOODOO.1*)
2.776 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
2.777 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
2.778 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
2.779 -(*EP- 11*)
2.780 -val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.781 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.782 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.783 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.784 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.785 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.786 -
2.787 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.788 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.789 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.790 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.791 -
2.792 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.793 -case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
2.794 - | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
2.795 -
2.796 -
2.797 -\<close> ML \<open>
2.798 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
2.799 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
2.800 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
2.801 -val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.802 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.803 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.804 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.805 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.806 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.807 -
2.808 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.809 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.810 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.811 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.812 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.813 -"TODO 1 + x + 2*x \<up> 2 = 0";
2.814 -"TODO 1 + x + 2*x \<up> 2 = 0";
2.815 -"TODO 1 + x + 2*x \<up> 2 = 0";
2.816 -
2.817 -
2.818 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
2.819 -val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.820 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.821 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.822 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.823 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.824 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.825 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.826 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.827 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.828 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.829 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.830 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
2.831 - | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
2.832 -
2.833 -\<close> ML \<open>
2.834 -val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.835 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.836 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.837 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.838 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.839 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.840 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.841 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.842 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.843 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.844 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.845 -"TODO 2 + 1*x + x \<up> 2 = 0";
2.846 -"TODO 2 + 1*x + x \<up> 2 = 0";
2.847 -"TODO 2 + 1*x + x \<up> 2 = 0";
2.848 -
2.849 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
2.850 -(*EP- 12*)
2.851 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.852 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.853 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.854 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.855 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.856 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.857 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.858 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.859 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.860 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.861 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.862 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
2.863 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
2.864 -
2.865 -\<close> ML \<open>
2.866 -val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.867 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.868 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.869 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.870 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.871 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.872 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.873 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.874 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.875 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.876 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.877 -"TODO 2 + x + x \<up> 2 = 0";
2.878 -"TODO 2 + x + x \<up> 2 = 0";
2.879 -"TODO 2 + x + x \<up> 2 = 0";
2.880 -
2.881 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
2.882 -(*EP- 13*)
2.883 -val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.884 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.885 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.886 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.887 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.888 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.889 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.890 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.891 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.892 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.893 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.894 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
2.895 - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
2.896 -
2.897 -\<close> ML \<open>
2.898 -val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.899 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.900 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.901 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.902 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.903 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.904 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.905 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.906 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.907 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.908 -"TODO 8+ 2*x \<up> 2 = 0";
2.909 -"TODO 8+ 2*x \<up> 2 = 0";
2.910 -"TODO 8+ 2*x \<up> 2 = 0";
2.911 -
2.912 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
2.913 -(*EP- 14*)
2.914 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.915 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.916 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.917 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.918 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.919 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.920 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.921 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.922 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.923 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.924 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
2.925 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
2.926 -
2.927 -
2.928 -\<close> ML \<open>
2.929 -val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.930 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.931 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.932 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.933 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.934 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.935 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.936 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.937 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.938 -"TODO 4+ x \<up> 2 = 0";
2.939 -"TODO 4+ x \<up> 2 = 0";
2.940 -"TODO 4+ x \<up> 2 = 0";
2.941 -
2.942 -\<close> text \<open> (*f = Test_Out.FormKF "[]"*)
2.943 -(*EP- 15*)
2.944 -val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.945 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.946 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.947 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.948 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.949 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.950 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.951 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.952 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.953 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.954 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.955 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.956 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
2.957 -
2.958 -\<close> text \<open> (* TOODOO.1*)
2.959 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.960 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.961 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.962 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.963 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.964 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.965 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.966 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.967 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.968 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.969 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.970 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.971 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
2.972 -
2.973 -\<close> text \<open> (* TOODOO.1 *)
2.974 -(*EP- 16*)
2.975 -val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.976 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.977 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.978 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.979 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.980 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.981 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.982 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.983 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.984 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.985 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.986 -case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
2.987 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
2.988 -
2.989 -\<close> ML \<open> (* loops*)
2.990 -(*EP-//*)
2.991 -val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
2.992 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
2.993 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
2.994 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.995 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.996 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.997 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.998 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.999 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1000 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1001 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1002 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
2.1003 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
2.1004 -
2.1005 -
2.1006 -\<close> text \<open> (* TOODOO.1 *)
2.1007 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
2.1008 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
2.1009 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
2.1010 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
2.1011 -see --- val rls = calculate_RootRat > calculate_Rational ---
2.1012 -calculate_RootRat was a TODO with 2002, requires re-design.
2.1013 -see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
2.1014 -*)
2.1015 - val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
2.1016 - "solveFor x", "solutions L"];
2.1017 - val (dI',pI',mI') =
2.1018 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
2.1019 - ["PolyEq", "complete_square"]);
2.1020 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.1021 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1022 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1023 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1024 -
2.1025 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1026 -(*Apply_Method ("PolyEq", "complete_square")*)
2.1027 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1028 -(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
2.1029 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1030 -(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
2.1031 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1032 -(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
2.1033 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1034 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
2.1035 - 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
2.1036 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1037 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
2.1038 - - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
2.1039 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1040 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
2.1041 - - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
2.1042 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1043 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
2.1044 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
2.1045 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1046 -(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
2.1047 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
2.1048 - NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
2.1049 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1050 -(*"x = - 2 | x = 4" nxt = Or_to_List*)
2.1051 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1052 -(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
2.1053 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
2.1054 -(* FIXXXME
2.1055 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
2.1056 - | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
2.1057 -*)
2.1058 -if f2str f =
2.1059 -"[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))]"
2.1060 -(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
2.1061 -then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
2.1062 -
2.1063 -
2.1064 -\<close> text \<open> (* TOODOO.1 *)
2.1065 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.1066 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.1067 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
2.1068 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
2.1069 -see --- val rls = calculate_RootRat > calculate_Rational ---*)
2.1070 -val thy = @ {theory PolyEq};
2.1071 -val ctxt = Proof_Context.init_global thy;
2.1072 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
2.1073 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
2.1074 -
2.1075 -val rls = complete_square;
2.1076 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
2.1077 -UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
2.1078 -
2.1079 -val thm = ThmC.numerals_to_Free @{thm square_explicit1};
2.1080 -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
2.1081 -UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
2.1082 -
2.1083 -val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
2.1084 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
2.1085 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.1086 - "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
2.1087 -
2.1088 -(*the thm bdv_explicit2* here required to be constrained to ::real*)
2.1089 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
2.1090 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.1091 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.1092 - "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
2.1093 -
2.1094 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
2.1095 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.1096 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
2.1097 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
2.1098 -
2.1099 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
2.1100 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
2.1101 -UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
2.1102 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
2.1103 -
2.1104 -val rls = calculate_RootRat;
2.1105 -val SOME (t,asm) = rewrite_set_ thy true rls t;
2.1106 -if UnparseC.term t =
2.1107 - "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"
2.1108 -(*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
2.1109 -then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
2.1110 -(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
2.1111 -
2.1112 -
2.1113 -\<close> ML \<open>
2.1114 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
2.1115 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
2.1116 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
2.1117 -"---- test the erls ----";
2.1118 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
2.1119 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
2.1120 - val t' = UnparseC.term t;
2.1121 - (*if t'= \<^const_name>\<open>True\<close> then ()
2.1122 - else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
2.1123 -(* *)
2.1124 - val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
2.1125 - "solveFor x", "solutions L"];
2.1126 - val (dI',pI',mI') =
2.1127 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
2.1128 - ["PolyEq", "complete_square"]);
2.1129 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.1130 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1131 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1132 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1133 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1134 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1135 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1136 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1137 - (*Apply_Method ("PolyEq", "complete_square")*)
2.1138 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
2.1139 -
2.1140 -\<close> text \<open> (* TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free" *)
2.1141 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
2.1142 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
2.1143 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
2.1144 - val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
2.1145 - "solveFor x", "solutions L"];
2.1146 - val (dI',pI',mI') =
2.1147 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
2.1148 - ["PolyEq", "complete_square"]);
2.1149 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.1150 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1151 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1152 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1153 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1154 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1155 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1156 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1157 - (*Apply_Method ("PolyEq", "complete_square")*)
2.1158 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1159 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1160 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1161 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1162 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1163 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1164 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1165 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1166 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1167 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.1168 -(* FIXXXXME n1.,
2.1169 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
2.1170 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
2.1171 -*)
2.1172 -
2.1173 -\<close> ML \<open>
2.1174 -\<close> text \<open> =======^^^^^ polyeq-1.sml------------vvv eqsystem.sml--------TOODOO-----------
2.1175 -\<close>
2.1176 -
2.1177 (** )ML_file \<open>Knowledge/eqsystem.sml\<close>( **)
2.1178 section \<open>======== check Knowledge/eqsystem.sml =============================================\<close>
2.1179 ML \<open>