1.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 02 15:27:47 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 02 15:30:41 2021 +0200
1.3 @@ -108,1176 +108,6 @@
1.4 \<close> ML \<open>
1.5 \<close>
1.6
1.7 -(** )ML_file \<open>Knowledge/polyeq-1.sml\<close>( **)
1.8 -section \<open>======== check Knowledge/polyeq-1.sml =============================================\<close>
1.9 -ML \<open>
1.10 -\<close> text \<open> =======-------------------------vvv polyeq-1.sml-------TOODOO----------------
1.11 -\<close> ML \<open>
1.12 -(* Title: Knowledge/polyeq-1.sml
1.13 - testexamples for PolyEq, poynomial equations and equational systems
1.14 - Author: Richard Lang 2003
1.15 - (c) due to copyright terms
1.16 -WN030609: some expls dont work due to unfinished handling of 'expanded terms';
1.17 - others marked with TODO have to be checked, too.
1.18 -*)
1.19 -
1.20 -"-----------------------------------------------------------------";
1.21 -"table of contents -----------------------------------------------";
1.22 -"-----------------------------------------------------------------";
1.23 -"------ polyeq- 1.sml ---------------------------------------------";
1.24 -"----------- tests on predicates in problems ---------------------";
1.25 -"----------- test matching problems ------------------------------";
1.26 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.27 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.28 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.29 -"----------- lin.eq degree_0 -------------------------------------";
1.30 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.31 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.32 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.33 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.34 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.35 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.36 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.37 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.38 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.39 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.40 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.41 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.42 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.43 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.44 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.45 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.46 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.47 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.48 -"-----------------------------------------------------------------";
1.49 -"------ polyeq- 2.sml ---------------------------------------------";
1.50 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.51 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.52 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.53 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.54 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.55 -"----------- rls make_polynomial_in ------------------------------";
1.56 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.57 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.58 -"-----------------------------------------------------------------";
1.59 -"-----------------------------------------------------------------";
1.60 -
1.61 -\<close> ML \<open>
1.62 -"----------- tests on predicates in problems ---------------------";
1.63 -"----------- tests on predicates in problems ---------------------";
1.64 -"----------- tests on predicates in problems ---------------------";
1.65 -Rewrite.trace_on:=false; (*true false*)
1.66 -
1.67 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.68 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.69 - if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
1.70 - else error "polyeq.sml: diff.behav. in lhs";
1.71 -
1.72 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.73 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.74 - if (UnparseC.term t) = "True" then ()
1.75 - else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.76 -
1.77 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
1.78 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.79 - if (UnparseC.term t) = "False" then ()
1.80 - else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.81 -
1.82 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
1.83 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.84 - if (UnparseC.term t) = "True" then ()
1.85 - else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.86 -
1.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";
1.88 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.89 - if (UnparseC.term t) = "True" then ()
1.90 - else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.91 -
1.92 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
1.93 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.94 - if (UnparseC.term t) = "True" then ()
1.95 - else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.96 -
1.97 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.98 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.99 - if (UnparseC.term t) = "True" then ()
1.100 - else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.101 -
1.102 -\<close> ML \<open> (*TOODOO broken with repair ord_make_polynomial_in*)
1.103 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.104 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.105 - if (UnparseC.term t) = "False" then ()
1.106 - else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.107 -
1.108 -\<close> ML \<open>
1.109 - val t4 = (Thm.term_of o the o (TermC.parse thy))
1.110 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
1.111 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.112 - if (UnparseC.term t) = "False" then ()
1.113 - else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.114 -
1.115 -val t5 = (Thm.term_of o the o (TermC.parse thy))
1.116 - "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.117 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.118 - if (UnparseC.term t) = "True" then ()
1.119 - else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.120 -
1.121 -\<close> ML \<open> (* M_Match.match_pbl [expanded,univariate,equation] *)
1.122 -"----------- test matching problems --------------------------0---";
1.123 -"----------- test matching problems --------------------------0---";
1.124 -"----------- test matching problems --------------------------0---";
1.125 -val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.126 -if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
1.127 - M_Match.Matches' {Find = [Correct "solutions L"],
1.128 - With = [],
1.129 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
1.130 - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
1.131 - Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
1.132 - Relate = []}
1.133 -then () else error "M_Match.match_pbl [expanded,univariate,equation]";
1.134 -
1.135 -\<close> ML \<open>
1.136 -if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
1.137 - M_Match.Matches' {Find = [Correct "solutions L"],
1.138 - With = [],
1.139 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
1.140 - Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
1.141 - Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
1.142 -then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
1.143 -
1.144 -\<close> ML \<open>
1.145 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.146 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.147 -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.148 -(*##################################################################################
1.149 ------------ 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.150 -
1.151 - (*Aufgabe zum Einstieg in die Arbeit...*)
1.152 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
1.153 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.154 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.155 - UnparseC.term t;
1.156 - "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
1.157 - val SOME (t,_) =
1.158 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.159 - UnparseC.term t;
1.160 - "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
1.161 -(* bei Verwendung von "size_of-term" nach MG :*)
1.162 -(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
1.163 -
1.164 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
1.165 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
1.166 - UnparseC.term t;
1.167 - "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
1.168 -(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
1.169 -
1.170 - val SOME (t,_) =
1.171 - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.172 - UnparseC.term t;
1.173 - "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
1.174 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.175 - "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
1.176 -
1.177 - (*das rewriting l"asst sich beobachten mit
1.178 -Rewrite.trace_on := false; (*true false*)
1.179 - *)
1.180 -
1.181 -"------ 15.11.02 --------------------------";
1.182 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
1.183 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
1.184 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.185 -
1.186 -Rewrite.trace_on := false; (*true false*)
1.187 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.188 - val SOME (t,_) =
1.189 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.190 - UnparseC.term t;
1.191 - val SOME (t,_) =
1.192 - rewrite_set_ thy false discard_parentheses t;
1.193 - UnparseC.term t;
1.194 -"1 + b * x + x * a";
1.195 -
1.196 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
1.197 - val SOME (t,_) =
1.198 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.199 - UnparseC.term t;
1.200 - val SOME (t,_) =
1.201 - rewrite_set_ thy false discard_parentheses t;
1.202 - UnparseC.term t;
1.203 -"1 + (x + b * x) * a + a \<up> 2";
1.204 -
1.205 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
1.206 - val SOME (t,_) =
1.207 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.208 - UnparseC.term t;
1.209 - val SOME (t,_) =
1.210 - rewrite_set_ thy false discard_parentheses t;
1.211 - UnparseC.term t;
1.212 -"1 + b * a + (7 + x) * a \<up> 2";
1.213 -
1.214 -(* MG2003
1.215 - Prog_Expr.thy grundlegende Algebra
1.216 - Poly.thy Polynome
1.217 - Rational.thy Br"uche
1.218 - Root.thy Wurzeln
1.219 - RootRat.thy Wurzen + Br"uche
1.220 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
1.221 -
1.222 - get_thm Termorder.thy "bdv_n_collect";
1.223 - get_thm (theory "Isac_Knowledge") "bdv_n_collect";
1.224 -*)
1.225 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
1.226 - val SOME (t,_) =
1.227 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.228 - UnparseC.term t;
1.229 - val SOME (t,_) =
1.230 - rewrite_set_ thy false discard_parentheses t;
1.231 - UnparseC.term t;
1.232 -"(7 + x) * a \<up> 2";
1.233 -
1.234 - val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
1.235 -
1.236 - val t = (Thm.term_of o the o (parseold thy)) "7";
1.237 -##################################################################################*)
1.238 -
1.239 -
1.240 -\<close> ML \<open>
1.241 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.242 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.243 -"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.244 -(* termorder hacked by MG, adapted later by WN *)
1.245 -(** )local ( *. for make_polynomial_in .*)
1.246 -
1.247 -open Term; (* for type order = EQUAL | LESS | GREATER *)
1.248 -
1.249 -fun pr_ord EQUAL = "EQUAL"
1.250 - | pr_ord LESS = "LESS"
1.251 - | pr_ord GREATER = "GREATER";
1.252 -
1.253 -fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
1.254 - | dest_hd' x (t as Free (a, T)) =
1.255 - if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
1.256 - else (((a, 0), T), 1)
1.257 - | dest_hd' _ (Var v) = (v, 2)
1.258 - | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
1.259 - | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
1.260 - | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
1.261 -
1.262 -fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
1.263 - Free (var, _) $ Free (pot, _)) =
1.264 - (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
1.265 - case x of (*WN*)
1.266 - (Free (xstr, _)) =>
1.267 - if xstr = var
1.268 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
1.269 - 1000 * (the (TermC.int_opt_of_string pot)))
1.270 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
1.271 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.272 - | size_of_term' i pr x (t as Abs (_, _, body)) =
1.273 - (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
1.274 - 1 + size_of_term' (i + 1) pr x body)
1.275 - | size_of_term' i pr x (f $ t) =
1.276 - let
1.277 - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
1.278 - val s1 = size_of_term' (i + 1) pr x f
1.279 - val s2 = size_of_term' (i + 1) pr x t
1.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 ();
1.281 - in (s1 + s2) end
1.282 - | size_of_term' i pr x t =
1.283 - (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
1.284 - case t of
1.285 - Free (subst, _) =>
1.286 - (case x of
1.287 - Free (xstr, _) =>
1.288 - if xstr = subst
1.289 - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
1.290 - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
1.291 - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.292 - | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
1.293 -
1.294 -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.295 - let
1.296 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
1.297 - val ord =
1.298 - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
1.299 - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
1.300 - in ord end
1.301 - | term_ord' i pr x _ (t, u) =
1.302 - let
1.303 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
1.304 - val ord =
1.305 - case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
1.306 - EQUAL =>
1.307 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1.308 - in
1.309 - (case hd_ord (i + 1) pr x (f, g) of
1.310 - EQUAL => (terms_ord x (i + 1) pr) (ts, us)
1.311 - | ord => ord)
1.312 - end
1.313 - | ord => ord
1.314 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
1.315 - in ord end
1.316 -and hd_ord i pr x (f, g) = (* ~ term.ML *)
1.317 - let
1.318 - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
1.319 - val ord = prod_ord
1.320 - (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
1.321 - (dest_hd' x f, dest_hd' x g)
1.322 - val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
1.323 - in ord end
1.324 -and terms_ord x i pr (ts, us) =
1.325 - let
1.326 - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
1.327 - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1.328 - val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
1.329 - in ord end
1.330 -
1.331 -(** )in( *local*)
1.332 -
1.333 -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
1.334 - ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
1.335 - case subst of
1.336 - (_, x) :: _ =>
1.337 - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
1.338 - | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
1.339 -
1.340 -(** )end;( *local*)
1.341 -
1.342 -\<close> ML \<open>
1.343 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.344 -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
1.345 -
1.346 -val x = TermC.str2term "x ::real";
1.347 -
1.348 -\<close> ML \<open>
1.349 -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
1.350 -if 2006 = size_of_term' 1 true x t1
1.351 -then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
1.352 -
1.353 -\<close> ML \<open>
1.354 -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
1.355 -if 3004 = size_of_term' 1 true x t2
1.356 -then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
1.357 -
1.358 -
1.359 -\<close> ML \<open>
1.360 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.361 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.362 -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.363 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
1.364 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
1.365 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
1.366 -
1.367 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
1.368 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.369 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.370 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
1.371 -
1.372 -\<close> ML \<open>
1.373 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
1.374 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
1.375 -
1.376 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
1.377 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
1.378 -
1.379 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.380 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.381 -
1.382 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.383 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.384 - ord_make_polynomial_in true thy substx (aa, bb);
1.385 - true; (* => LESS *)
1.386 -
1.387 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.388 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.389 - ord_make_polynomial_in true thy substa (aa, bb);
1.390 - false; (* => GREATER *)
1.391 -
1.392 -\<close> ML \<open>
1.393 -(* und nach dem Re-engineering der Termorders in den 'rulesets'
1.394 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
1.395 - val bdv= TermC.str2term "bdv ::real";
1.396 - val x = TermC.str2term "x ::real";
1.397 - val a = TermC.str2term "a ::real";
1.398 - val b = TermC.str2term "b ::real";
1.399 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.400 -if UnparseC.term t' = "b + x + a" then ()
1.401 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.402 -
1.403 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
1.404 -
1.405 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
1.406 -if UnparseC.term t' = "a + b + x" then ()
1.407 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.408 -
1.409 -\<close> ML \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
1.410 - val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
1.411 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.412 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.413 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
1.414 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.415 -
1.416 -\<close> ML \<open>
1.417 - val ttt' = "(3*x + 5)/18 ::real";
1.418 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
1.419 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.420 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.421 -else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.422 -
1.423 -\<close> ML \<open>
1.424 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.425 -if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.426 -else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.427 -
1.428 -\<close> ML \<open>
1.429 -"----------- lin.eq degree_0 -------------------------------------";
1.430 -"----------- lin.eq degree_0 -------------------------------------";
1.431 -"----------- lin.eq degree_0 -------------------------------------";
1.432 -"----- d0_false ------";
1.433 -val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
1.434 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
1.435 - ["PolyEq", "solve_d0_polyeq_equation"]);
1.436 -(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
1.437 -TODO: change to "equality (x + - 1*x = (0::real))"
1.438 - and search for an appropriate problem and method.
1.439 -
1.440 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.441 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.442 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.443 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.444 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.445 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.446 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.447 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.448 - | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.449 -
1.450 -"----- d0_true ------";
1.451 -val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
1.452 -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
1.453 - ["PolyEq", "solve_d0_polyeq_equation"]);
1.454 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.455 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.456 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.457 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.458 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.459 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.460 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.461 -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
1.462 - | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
1.463 -============ inhibit exn WN110914 ============================================*)
1.464 -
1.465 -\<close> text \<open>
1.466 -(*rewrite_set_, rewrite_ "- 1 / 4 = - 1 / 4" z =
1.467 -- 1 * (- 1 / 4 / 2) + sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2 \<or>
1.468 -z =
1.469 -- 1 * (- 1 / 4 / 2) + - 1 * (sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2) = NONE*)
1.470 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.471 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.472 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.473 -"----- d2_pqformula1 ------!!!!";
1.474 -val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
1.475 -val (dI',pI',mI') =
1.476 - ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
1.477 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.478 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.479 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.480 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.481 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.482 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.483 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.484 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
1.485 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.486 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.487 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.488 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.489 -
1.490 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.491 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.492 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.493 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.494 -
1.495 -if p = ([], Res) andalso
1.496 - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
1.497 - case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
1.498 -else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
1.499 -
1.500 -\<close> ML \<open>
1.501 -Rewrite.trace_on := false; (*true false*)
1.502 -\<close> ML \<open>
1.503 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.504 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.505 -"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.506 -"----- d2_pqformula1_neg ------";
1.507 -val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
1.508 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.509 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.510 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.511 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.512 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.513 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.514 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.515 -(*### or2list False
1.516 - ([1],Res) False Or_to_List)*)
1.517 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.518 -(*### or2list False
1.519 - ([2],Res) [] Check_elementwise "Assumptions"*)
1.520 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.521 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.522 -val asm = Ctree.get_assumptions pt p;
1.523 -if f2str f = "[]" andalso
1.524 - UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
1.525 - "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
1.526 -else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
1.527 -
1.528 -\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
1.529 -x = - 1 * (- 1 / 2) + - 1 * (sqrt ((- 1) \<up> 2 + 8) / 2) = NONE*)
1.530 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.531 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.532 -"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.533 -"----- d2_pqformula2 ------";
1.534 -val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.535 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.536 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.537 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.538 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.539 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.540 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.541 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.542 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.543 -
1.544 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.545 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.546 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.547 -case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
1.548 - | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
1.549 -
1.550 -
1.551 -\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
1.552 -exception TYPE raised (line 169 of "consts.ML"): Illegal type for constant "HOL.eq" :: real
1.553 - \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool*)
1.554 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.555 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.556 -"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.557 -"----- d2_pqformula3 ------";
1.558 -(*EP-9*)
1.559 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.560 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.561 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.562 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.563 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.564 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.565 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.566 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.567 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.568 -
1.569 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.570 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.571 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.572 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.573 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
1.574 -
1.575 -
1.576 -\<close> ML \<open>
1.577 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.578 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.579 -"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.580 -"----- d2_pqformula3_neg ------";
1.581 -val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.582 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.583 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.584 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.585 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.586 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.587 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.588 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.589 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.590 -
1.591 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.592 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.593 -"TODO 2 + x + x \<up> 2 = 0";
1.594 -"TODO 2 + x + x \<up> 2 = 0";
1.595 -"TODO 2 + x + x \<up> 2 = 0";
1.596 -
1.597 -\<close> text \<open> (*see TOODOO.1*)
1.598 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.599 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.600 -"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.601 -"----- d2_pqformula4 ------";
1.602 -val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.603 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.604 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.605 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.606 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.607 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.608 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.609 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.610 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.611 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.612 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.613 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.614 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.615 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
1.616 -
1.617 -\<close> text \<open> (* FormKF "[]" instead of "[x = 0, x = - 1]"*)
1.618 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.619 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.620 -"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.621 -"----- d2_pqformula5 ------";
1.622 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.623 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.624 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.625 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.626 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.627 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.628 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.629 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.630 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.631 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.632 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.633 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.634 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.635 - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
1.636 -
1.637 -\<close> text \<open> (* TOODOO.1 *)
1.638 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.639 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.640 -"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.641 -"----- d2_pqformula6 ------";
1.642 -val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.643 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.644 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.645 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.646 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.647 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.648 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.649 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.650 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.651 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.652 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.653 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.654 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.655 - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
1.656 -
1.657 -\<close> text \<open> (* TOODOO.1*)
1.658 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.659 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.660 -"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.661 -"----- d2_pqformula7 ------";
1.662 -(*EP- 10*)
1.663 -val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.664 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.665 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.666 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.667 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.668 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.669 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.670 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.671 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.672 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.673 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.674 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.675 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.676 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.677 -
1.678 -\<close> text \<open> (* TOODOO.1*)
1.679 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.680 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.681 -"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.682 -"----- d2_pqformula8 ------";
1.683 -val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.684 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.685 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.686 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.687 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.688 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.689 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.690 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.691 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.692 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.693 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.694 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.695 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.696 - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
1.697 -
1.698 -\<close> text \<open> (* TOODOO.1*)
1.699 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.700 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.701 -"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.702 -"----- d2_pqformula9 ------";
1.703 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.704 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.705 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.706 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.707 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.708 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.709 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.710 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.711 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.712 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.713 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.714 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.715 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
1.716 -
1.717 -
1.718 -\<close> ML \<open>
1.719 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.720 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.721 -"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.722 -"----- d2_pqformula9_neg ------";
1.723 -val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.724 -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.725 - ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.726 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.727 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.728 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.729 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.730 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.731 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.732 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.733 -"TODO 4 + 1*x \<up> 2 = 0";
1.734 -"TODO 4 + 1*x \<up> 2 = 0";
1.735 -"TODO 4 + 1*x \<up> 2 = 0";
1.736 -
1.737 -\<close> text \<open> (*see TOODOO.1*)
1.738 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.739 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.740 -"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.741 -val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.742 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.743 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.744 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.745 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.746 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.747 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.748 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.749 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.750 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.751 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.752 -case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
1.753 - | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
1.754 -
1.755 -\<close> ML \<open>
1.756 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.757 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.758 -"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.759 -val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.760 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.761 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.762 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.763 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.764 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.765 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.766 -
1.767 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.768 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.769 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.770 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.771 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.772 -"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.773 -
1.774 -
1.775 -\<close> text \<open> (*see TOODOO.1*)
1.776 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.777 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.778 -"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.779 -(*EP- 11*)
1.780 -val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.781 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.782 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.783 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.784 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.785 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.786 -
1.787 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.788 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.789 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.790 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.791 -
1.792 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.793 -case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
1.794 - | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
1.795 -
1.796 -
1.797 -\<close> ML \<open>
1.798 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.799 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.800 -"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.801 -val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.802 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.803 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.804 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.805 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.806 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.807 -
1.808 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.809 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.810 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.811 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.812 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.813 -"TODO 1 + x + 2*x \<up> 2 = 0";
1.814 -"TODO 1 + x + 2*x \<up> 2 = 0";
1.815 -"TODO 1 + x + 2*x \<up> 2 = 0";
1.816 -
1.817 -
1.818 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
1.819 -val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.820 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.821 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.822 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.823 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.824 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.825 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.826 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.827 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.828 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.829 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.830 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.831 - | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
1.832 -
1.833 -\<close> ML \<open>
1.834 -val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.835 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.836 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.837 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.838 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.839 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.840 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.841 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.842 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.843 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.844 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.845 -"TODO 2 + 1*x + x \<up> 2 = 0";
1.846 -"TODO 2 + 1*x + x \<up> 2 = 0";
1.847 -"TODO 2 + 1*x + x \<up> 2 = 0";
1.848 -
1.849 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
1.850 -(*EP- 12*)
1.851 -val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.852 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.853 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.854 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.855 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.856 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.857 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.858 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.859 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.860 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.861 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.862 -case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.863 - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
1.864 -
1.865 -\<close> ML \<open>
1.866 -val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.867 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.868 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.869 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.870 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.871 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.872 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.873 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.874 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.875 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.876 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.877 -"TODO 2 + x + x \<up> 2 = 0";
1.878 -"TODO 2 + x + x \<up> 2 = 0";
1.879 -"TODO 2 + x + x \<up> 2 = 0";
1.880 -
1.881 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
1.882 -(*EP- 13*)
1.883 -val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.884 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.885 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.886 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.887 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.888 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.889 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.890 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.891 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.892 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.893 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.894 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.895 - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
1.896 -
1.897 -\<close> ML \<open>
1.898 -val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.899 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.900 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.901 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.902 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.903 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.904 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.905 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.906 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.907 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.908 -"TODO 8+ 2*x \<up> 2 = 0";
1.909 -"TODO 8+ 2*x \<up> 2 = 0";
1.910 -"TODO 8+ 2*x \<up> 2 = 0";
1.911 -
1.912 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
1.913 -(*EP- 14*)
1.914 -val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.915 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.916 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.917 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.918 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.919 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.920 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.921 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.922 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.923 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.924 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.925 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
1.926 -
1.927 -
1.928 -\<close> ML \<open>
1.929 -val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.930 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.931 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.932 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.933 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.934 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.935 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.936 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.937 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.938 -"TODO 4+ x \<up> 2 = 0";
1.939 -"TODO 4+ x \<up> 2 = 0";
1.940 -"TODO 4+ x \<up> 2 = 0";
1.941 -
1.942 -\<close> text \<open> (*f = Test_Out.FormKF "[]"*)
1.943 -(*EP- 15*)
1.944 -val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.945 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.946 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.947 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.948 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.949 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.950 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.951 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.952 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.953 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.954 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.955 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.956 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.957 -
1.958 -\<close> text \<open> (* TOODOO.1*)
1.959 -val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.960 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.961 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.962 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.963 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.964 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.965 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.966 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.967 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.968 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.969 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.970 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.971 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.972 -
1.973 -\<close> text \<open> (* TOODOO.1 *)
1.974 -(*EP- 16*)
1.975 -val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.976 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.977 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.978 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.979 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.980 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.981 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.982 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.983 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.984 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.985 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.986 -case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
1.987 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
1.988 -
1.989 -\<close> ML \<open> (* loops*)
1.990 -(*EP-//*)
1.991 -val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.992 -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.993 - ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.994 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.995 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.996 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.997 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.998 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.999 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1000 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1001 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1002 -case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.1003 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.1004 -
1.1005 -
1.1006 -\<close> text \<open> (* TOODOO.1 *)
1.1007 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.1008 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.1009 -"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.1010 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.1011 -see --- val rls = calculate_RootRat > calculate_Rational ---
1.1012 -calculate_RootRat was a TODO with 2002, requires re-design.
1.1013 -see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
1.1014 -*)
1.1015 - val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.1016 - "solveFor x", "solutions L"];
1.1017 - val (dI',pI',mI') =
1.1018 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.1019 - ["PolyEq", "complete_square"]);
1.1020 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1021 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1022 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1023 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1024 -
1.1025 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1026 -(*Apply_Method ("PolyEq", "complete_square")*)
1.1027 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1028 -(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.1029 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1030 -(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
1.1031 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1032 -(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
1.1033 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1034 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1.1035 - 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.1036 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1037 -(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1.1038 - - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.1039 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1040 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.1041 - - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
1.1042 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1043 -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.1044 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
1.1045 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1046 -(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
1.1047 - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
1.1048 - NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
1.1049 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1050 -(*"x = - 2 | x = 4" nxt = Or_to_List*)
1.1051 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1052 -(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
1.1053 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.1054 -(* FIXXXME
1.1055 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
1.1056 - | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1.1057 -*)
1.1058 -if f2str f =
1.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))]"
1.1060 -(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1.1061 -then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1.1062 -
1.1063 -
1.1064 -\<close> text \<open> (* TOODOO.1 *)
1.1065 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.1066 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.1067 -"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.1068 -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.1069 -see --- val rls = calculate_RootRat > calculate_Rational ---*)
1.1070 -val thy = @ {theory PolyEq};
1.1071 -val ctxt = Proof_Context.init_global thy;
1.1072 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1.1073 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1.1074 -
1.1075 -val rls = complete_square;
1.1076 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.1077 -UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
1.1078 -
1.1079 -val thm = ThmC.numerals_to_Free @{thm square_explicit1};
1.1080 -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.1081 -UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
1.1082 -
1.1083 -val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1.1084 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.1085 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.1086 - "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.1087 -
1.1088 -(*the thm bdv_explicit2* here required to be constrained to ::real*)
1.1089 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.1090 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.1091 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.1092 - "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.1093 -
1.1094 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1.1095 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.1096 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.1097 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.1098 -
1.1099 -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.1100 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.1101 -UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1.1102 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.1103 -
1.1104 -val rls = calculate_RootRat;
1.1105 -val SOME (t,asm) = rewrite_set_ thy true rls t;
1.1106 -if UnparseC.term t =
1.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))"
1.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*)
1.1109 -then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.1110 -(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
1.1111 -
1.1112 -
1.1113 -\<close> ML \<open>
1.1114 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.1115 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.1116 -"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.1117 -"---- test the erls ----";
1.1118 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
1.1119 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.1120 - val t' = UnparseC.term t;
1.1121 - (*if t'= \<^const_name>\<open>True\<close> then ()
1.1122 - else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.1123 -(* *)
1.1124 - val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
1.1125 - "solveFor x", "solutions L"];
1.1126 - val (dI',pI',mI') =
1.1127 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.1128 - ["PolyEq", "complete_square"]);
1.1129 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1130 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1131 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1132 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1133 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1134 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1135 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1136 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1137 - (*Apply_Method ("PolyEq", "complete_square")*)
1.1138 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.1139 -
1.1140 -\<close> text \<open> (* TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free" *)
1.1141 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.1142 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.1143 -"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.1144 - val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
1.1145 - "solveFor x", "solutions L"];
1.1146 - val (dI',pI',mI') =
1.1147 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.1148 - ["PolyEq", "complete_square"]);
1.1149 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1150 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1151 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1152 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1153 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1154 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1155 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1156 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1157 - (*Apply_Method ("PolyEq", "complete_square")*)
1.1158 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1159 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1160 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1161 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1162 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1163 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1164 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1165 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1166 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1167 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1168 -(* FIXXXXME n1.,
1.1169 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1.1170 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1.1171 -*)
1.1172 -
1.1173 -\<close> ML \<open>
1.1174 -\<close> text \<open> =======^^^^^ polyeq-1.sml------------vvv eqsystem.sml--------TOODOO-----------
1.1175 -\<close>
1.1176 -
1.1177 (** )ML_file \<open>Knowledge/eqsystem.sml\<close>( **)
1.1178 section \<open>======== check Knowledge/eqsystem.sml =============================================\<close>
1.1179 ML \<open>