diff -r 63cecf440235 -r 40eb8aa2b0d6 test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Jun 21 22:08:01 2021 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Jul 18 18:15:27 2021 +0200 @@ -1,4 +1,4 @@ -(* Title: Knowledge/polyeq-1.sml +(* Title: Knowledge/polyeq- 1.sml testexamples for PolyEq, poynomial equations and equational systems Author: Richard Lang 2003 (c) due to copyright terms @@ -9,36 +9,36 @@ "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; -"------ polyeq-1.sml ---------------------------------------------"; +"------ polyeq- 1.sml ---------------------------------------------"; "----------- tests on predicates in problems ---------------------"; "----------- test matching problems ------------------------------"; "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; "----------- lin.eq degree_0 -------------------------------------"; "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; -"----------- equality (2 +(-1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (-2 +(-1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (-2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; "----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (-2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; "----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; "----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; "----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; "----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; "----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; "----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (1 +(-1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (-1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; "----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; "----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; "----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -"----------- (-16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; "-----------------------------------------------------------------"; -"------ polyeq-2.sml ---------------------------------------------"; +"------ polyeq- 2.sml ---------------------------------------------"; "----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; "----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; -"----------- (-147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; +"----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; "----------- ((x+1)*(x+2) - (3*x - 2) \ 2=.. Schalk II s.68 Bsp 37"; "----------- rls make_polynomial_in ------------------------------"; "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; @@ -49,9 +49,8 @@ "----------- tests on predicates in problems ---------------------"; "----------- tests on predicates in problems ---------------------"; "----------- tests on predicates in problems ---------------------"; -(* Rewrite.trace_on:=true; - Rewrite.trace_on:=false; -*) +Rewrite.trace_on:=true; (*true false*) + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \ 2 = 0)"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; if ((UnparseC.term t) = "-8 - 2 * x + x \ 2") then () @@ -67,12 +66,12 @@ if (UnparseC.term t) = "False" then () else error "polyeq.sml: diff.behav. 2 in is_poly_in"; - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x \ 2) is_poly_in x"; + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \ 2) is_poly_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 3 in is_poly_in"; - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x \ 2 = 0)) is_expanded_in x"; + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \ 2 = 0)) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; if (UnparseC.term t) = "True" then () else error "polyeq.sml: diff.behav. 4 in is_expended_in"; @@ -131,44 +130,44 @@ "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; (*################################################################################## ------------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy +----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy (*Aufgabe zum Einstieg in die Arbeit...*) val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \ 2 = 0"; (*ein 'ruleset' aus Poly.ML wird angewandt...*) val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; UnparseC.term t; - "a * b + (-1 * (a * x) + (-1 * (b * x) + x \ 2)) = 0"; + "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \ 2)) = 0"; val SOME (t,_) = rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; UnparseC.term t; - "x \ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0"; + "x \ 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0"; (* bei Verwendung von "size_of-term" nach MG :*) -(*"x \ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *) +(*"x \ 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *) (*wir holen 'a' wieder aus der Klammerung heraus...*) val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; UnparseC.term t; - "x \ 2 + -1 * b * x + -1 * x * a + b * a = 0"; -(* "x \ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *) + "x \ 2 + - 1 * b * x + - 1 * x * a + b * a = 0"; +(* "x \ 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *) val SOME (t,_) = rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; UnparseC.term t; - "x \ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; + "x \ 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0"; (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben - "x \ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) + "x \ 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*) (*das rewriting l"asst sich beobachten mit -Rewrite.trace_on := false; +Rewrite.trace_on := false; (*true false*) *) -"------15.11.02 --------------------------"; +"------ 15.11.02 --------------------------"; val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x"; val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv"; val a = (Thm.term_of o the o (TermC.parse thy)) "a"; -Rewrite.trace_on := false; +Rewrite.trace_on := false; (*true false*) (* Anwenden einer Regelmenge aus Termorder.ML: *) val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; @@ -243,12 +242,12 @@ if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () else error "termorder.sml diff.behav ord_make_polynomial_in #3"; - val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x"; + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; ord_make_polynomial_in true thy substx (aa, bb); true; (* => LESS *) - val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x"; + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; ord_make_polynomial_in true thy substa (aa, bb); false; (* => GREATER *) @@ -269,14 +268,14 @@ if UnparseC.term t' = "a + b + x" then () else error "termorder.sml diff.behav ord_make_polynomial_in #13"; - val ppp' = "-6 + -5*x + x \ 3 + -1*x \ 2 + -1*x \ 3 + -14*x \ 2"; + val ppp' = "-6 + -5*x + x \ 3 + - 1*x \ 2 + - 1*x \ 3 + - 14*x \ 2"; val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp'; val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; -if UnparseC.term t' = "-6 + -5 * x + -15 * x \ 2 + 0" then () +if UnparseC.term t' = "-6 + -5 * x + - 15 * x \ 2 + 0" then () else error "termorder.sml diff.behav ord_make_polynomial_in #14"; val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; -if UnparseC.term t' = "-6 + -5 * x + -15 * x \ 2 + 0" then () +if UnparseC.term t' = "-6 + -5 * x + - 15 * x \ 2 + 0" then () else error "termorder.sml diff.behav ord_make_polynomial_in #15"; val ttt' = "(3*x + 5)/18"; @@ -300,7 +299,7 @@ val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d0_polyeq_equation"]); (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ======== -TODO: change to "equality (x + -1*x = (0::real))" +TODO: change to "equality (x + - 1*x = (0::real))" and search for an appropriate problem and method. val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -332,7 +331,7 @@ "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; "----- d2_pqformula1 ------!!!!"; -val fmz = ["equality (-1/8 + (-1/4)*z + z \ 2 = (0::real))", "solveFor z", "solutions L"]; +val fmz = ["equality (- 1/8 + (- 1/4)*z + z \ 2 = (0::real))", "solveFor z", "solutions L"]; val (dI',pI',mI') = ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -348,21 +347,21 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*) +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; if p = ([], Res) andalso - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]" then - case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z \ 2 = (0::real)) CHANGED 1" -else error "(-1/8 + (-1/4)*z + z \ 2 = (0::real)) CHANGED 2"; + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then + case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 1" +else error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 2"; -"----------- equality (2 +(-1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (2 +(-1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (2 +(-1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; +"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; "----- d2_pqformula1_neg ------"; -val fmz = ["equality (2 +(-1)*x + x \ 2 = (0::real))", "solveFor x", "solutions L"]; +val fmz = ["equality (2 +(- 1)*x + x \ 2 = (0::real))", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [] pt; @@ -379,15 +378,15 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val asm = Ctree.get_assumptions pt p; if f2str f = "[]" andalso - UnparseC.terms asm = "[\"lhs (2 + -1 * x + x \ 2 = 0) is_poly_in x\", " ^ - "\"lhs (2 + -1 * x + x \ 2 = 0) has_degree_in x = 2\"]" then () -else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x \ 2 = 0"; + UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \ 2 = 0) is_poly_in x\", " ^ + "\"lhs (2 + - 1 * x + x \ 2 = 0) has_degree_in x = 2\"]" then () +else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \ 2 = 0"; -"----------- equality (-2 +(-1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (-2 +(-1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (-2 +(-1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; +"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; "----- d2_pqformula2 ------"; -val fmz = ["equality (-2 +(-1)*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (- 2 +(- 1)*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -400,16 +399,16 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]"; +case f of Test_Out.FormKF "[x = 2, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]"; -"----------- equality (-2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----------- equality (-2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----------- equality (-2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; +"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; "----- d2_pqformula3 ------"; (*EP-9*) -val fmz = ["equality (-2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -422,8 +421,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]"; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]"; "----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; @@ -446,11 +445,11 @@ "TODO 2 + x + x \ 2 = 0"; "TODO 2 + x + x \ 2 = 0"; -"----------- equality (-2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----------- equality (-2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----------- equality (-2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; "----- d2_pqformula4 ------"; -val fmz = ["equality (-2 + x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (- 2 + x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -462,8 +461,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x \ 2 = 0 -> [x = 1, x = -2]"; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \ 2 = 0 -> [x = 1, x = - 2]"; "----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; "----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; @@ -481,8 +480,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]"; "----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; "----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; @@ -500,14 +499,14 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]"; "----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; "----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; "----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; "----- d2_pqformula7 ------"; -(*EP-10*) +(*EP- 10*) val fmz = ["equality ( x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); @@ -520,8 +519,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; "----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; "----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; @@ -539,8 +538,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]"; "----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; "----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; @@ -557,8 +556,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; "----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; @@ -582,7 +581,7 @@ "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; -val fmz = ["equality (-1 +(-1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (- 1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -593,13 +592,13 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = -1 / 2]" => () - | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]"; +case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]"; -"----------- equality (1 +(-1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (1 +(-1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (1 +(-1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -val fmz = ["equality (1 +(-1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; +val fmz = ["equality (1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -610,16 +609,16 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 1 +(-1)*x + 2*x \ 2 = 0"; -"TODO 1 +(-1)*x + 2*x \ 2 = 0"; -"TODO 1 +(-1)*x + 2*x \ 2 = 0"; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; +"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; -"----------- equality (-1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -"----------- equality (-1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -"----------- equality (-1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -(*EP-11*) -val fmz = ["equality (-1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; +(*EP- 11*) +val fmz = ["equality (- 1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -632,8 +631,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1 / 2, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]"; +case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]"; "----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; @@ -656,7 +655,7 @@ "TODO 1 + x + 2*x \ 2 = 0"; -val fmz = ["equality (-2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (- 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -667,8 +666,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]"; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]"; val fmz = ["equality ( 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], @@ -685,8 +684,8 @@ "TODO 2 + 1*x + x \ 2 = 0"; "TODO 2 + 1*x + x \ 2 = 0"; -(*EP-12*) -val fmz = ["equality (-2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; +(*EP- 12*) +val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -697,8 +696,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]"; +case f of Test_Out.FormKF "[x = 1, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]"; val fmz = ["equality ( 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], @@ -715,7 +714,7 @@ "TODO 2 + x + x \ 2 = 0"; "TODO 2 + x + x \ 2 = 0"; -(*EP-13*) +(*EP- 13*) val fmz = ["equality (-8 + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); @@ -727,8 +726,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]"; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]"; val fmz = ["equality ( 8+ 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], @@ -744,7 +743,7 @@ "TODO 8+ 2*x \ 2 = 0"; "TODO 8+ 2*x \ 2 = 0"; -(*EP-14*) +(*EP- 14*) val fmz = ["equality (-4 + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -755,8 +754,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = -2]" => () - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; val fmz = ["equality ( 4+ x \ 2 = 0)", "solveFor x", "solutions L"]; @@ -772,7 +771,7 @@ "TODO 4+ x \ 2 = 0"; "TODO 4+ x \ 2 = 0"; -(*EP-15*) +(*EP- 15*) val fmz = ["equality (2*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); @@ -784,8 +783,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; val fmz = ["equality (1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], @@ -798,10 +797,10 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; -(*EP-16*) +(*EP- 16*) val fmz = ["equality (x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); @@ -813,8 +812,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1 / 2]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]"; +case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]"; (*EP-//*) val fmz = ["equality (x + x \ 2 = 0)", "solveFor x", "solutions L"]; @@ -828,8 +827,8 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = -1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; +case f of Test_Out.FormKF "[x = 0, x = - 1]" => () + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; "----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; @@ -863,30 +862,30 @@ 2 / 2 - x = - sqrt ((2 / 2) \ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) | - -1*x = - (2 / 2) + - sqrt ((2 / 2) \ 2 - -8)"nxt = R_Inst("bdv_explt2"*) + - 1*x = - (2 / 2) + - sqrt ((2 / 2) \ 2 - -8)"nxt = R_Inst("bdv_explt2"*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | - -1 * x = (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = bdv_explicit3*) +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | + - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = bdv_explicit3*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))" nxt = bdv_explicit3*) +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))" nxt = bdv_explicit3*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) \ 2 - -8)) | - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = calculate_Rational +(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \ 2 - -8)) | + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = calculate_Rational NOT IMPLEMENTED SINCE 2002 ------------------------------ \ \ \ \ \ \ *) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"x = -2 | x = 4" nxt = Or_to_List*) +(*"x = - 2 | x = 4" nxt = Or_to_List*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"[x = -2, x = 4]" nxt = Check_Postcond*) +(*"[x = - 2, x = 4]" nxt = Check_Postcond*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; (* FIXXXME - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO - | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]"; + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO + | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]"; *) if f2str f = -"[x = -1 * -1 + -1 * sqrt (2 \ 2 / 2 \ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 \ 2 / 2 \ 2 - -8))]" -(*"[x = -1 * -1 + -1 * sqrt (1 \ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 \ 2 - -8))]"*) -then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]"; +"[x = - 1 * - 1 + - 1 * sqrt (2 \ 2 / 2 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))]" +(*"[x = - 1 * - 1 + - 1 * sqrt (1 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \ 2 - -8))]"*) +then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]"; "----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; @@ -910,31 +909,31 @@ val thm = ThmC.numerals_to_Free @{thm root_plus_minus}; val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\n2 / 2 - x = -1 * sqrt ((2 / 2) \ 2 - -8)"; + "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \ 2 - -8)"; (*the thm bdv_explicit2* here required to be constrained to ::real*) val thm = ThmC.numerals_to_Free @{thm bdv_explicit2}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) \ 2 - -8)"; + "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8)"; val thm = ThmC.numerals_to_Free @{thm bdv_explicit3}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \ 2 - -8))"; + "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8))"; val thm = ThmC.numerals_to_Free @{thm bdv_explicit2}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) |"^ - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \ 2 - -8))"; +UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) |"^ + "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8))"; val rls = calculate_RootRat; val SOME (t,asm) = rewrite_set_ thy true rls t; if UnparseC.term t = - "-1 * x = -1 + sqrt (2 \ 2 / 2 \ 2 - -8) \\nx = -1 * -1 + -1 * (-1 * sqrt (2 \ 2 / 2 \ 2 - -8))" -(*"-1 * x = -1 + sqrt (2 \ 2 / 2 \ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 \ 2 / 2 \ 2 - -8))"..isabisac15*) + "- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) \\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))" +(*"- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))"..isabisac15*) then () else error "(-8 - 2*x + x \ 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; -(*SHOULD BE: UnparseC.term = "x = -2 | x = 4;*) +(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) "-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; @@ -963,10 +962,10 @@ (*Apply_Method ("PolyEq", "complete_square")*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; -"----------- (-16 + 4*x + 2*x \ 2 = 0), --------------------------"; -"----------- (-16 + 4*x + 2*x \ 2 = 0), --------------------------"; -"----------- (-16 + 4*x + 2*x \ 2 = 0), --------------------------"; - val fmz = ["equality (-16 + 4*x + 2*x \ 2 = 0)", +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; +"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; + val fmz = ["equality (- 16 + 4*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["degree_2", "expanded", "univariate", "equation"],