walther@59627: (* Title:  Knowledge/polyeq-1.sml
walther@59627:            testexamples for PolyEq, poynomial equations and equational systems
walther@59627:    Author: Richard Lang 2003  
walther@59627:    (c) due to copyright terms
walther@59627: WN030609: some expls dont work due to unfinished handling of 'expanded terms';
walther@59627:           others marked with TODO have to be checked, too.
walther@59627: *)
walther@59627: 
walther@59627: "-----------------------------------------------------------------";
walther@59627: "table of contents -----------------------------------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: "------ polyeq-1.sml ---------------------------------------------";
walther@59627: "----------- tests on predicates in problems ---------------------";
walther@59627: "----------- test matching problems ------------------------------";
walther@59847: "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
walther@59847: "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
walther@59627: "----------- lin.eq degree_0 -------------------------------------";
walther@59627: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
walther@60242: "----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
walther@60242: "----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
walther@60242: "----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
walther@60242: "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
walther@60242: "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
walther@60242: "----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
walther@60242: "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";
walther@60242: "----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: "------ polyeq-2.sml ---------------------------------------------";
walther@60242: "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
walther@60242: "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
walther@60242: "----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
walther@59627: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
walther@60242: "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
walther@59627: "----------- rls make_polynomial_in ------------------------------";
walther@59627: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
walther@59627: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: 
walther@59627: "----------- tests on predicates in problems ---------------------";
walther@59627: "----------- tests on predicates in problems ---------------------";
walther@59627: "----------- tests on predicates in problems ---------------------";
walther@59901: (* Rewrite.trace_on:=true;
walther@59901:  Rewrite.trace_on:=false;
walther@59627: *)
walther@60242:  val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
walther@60242:  if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
walther@59627:  else  error "polyeq.sml: diff.behav. in lhs";
walther@59627: 
walther@60242:  val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 1 in is_expended_in";
walther@59627: 
walther@60230:  val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
walther@59868:  if (UnparseC.term t) = "False" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 2 in is_poly_in";
walther@59627: 
walther@60242:  val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x \<up> 2) is_poly_in x";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 3 in is_poly_in";
walther@59627: 
walther@60242:  val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
walther@59627: 
walther@59627: 
walther@60242:  val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 5 in is_expended_in";
walther@59627:  
walther@60242:  val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. in has_degree_in_in";
walther@59627: 
walther@60230:  val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
walther@59868:  if (UnparseC.term t) = "False" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
walther@59627: 
walther@60230:  val t4 = (Thm.term_of o the o (TermC.parse thy)) 
walther@60242: 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
walther@59868:  if (UnparseC.term t) = "False" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
walther@59627: 
walther@60230:  val t5 = (Thm.term_of o the o (TermC.parse thy)) 
walther@60242: 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
walther@59868:  if (UnparseC.term t) = "True" then ()
walther@59627:  else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
walther@59627: 
walther@59627: "----------- test matching problems --------------------------0---";
walther@59627: "----------- test matching problems --------------------------0---";
walther@59627: "----------- test matching problems --------------------------0---";
walther@60242: val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
walther@59984:   M_Match.Matches' {Find = [Correct "solutions L"], 
walther@59627:             With = [], 
walther@60242:             Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
walther@60242:             Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)", 
walther@60242:                      Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 
walther@59627:             Relate = []}
walther@59984: then () else error "M_Match.match_pbl [expanded,univariate,equation]";
walther@59627: 
walther@59997: if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
walther@59984:   M_Match.Matches' {Find = [Correct "solutions L"], 
walther@59627:             With = [], 
walther@60242:             Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
walther@60242:             Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 
walther@59627:             Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)
walther@59984: then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
walther@59627: 
walther@59847: 
walther@59847: "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
walther@59847: "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
walther@59847: "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
walther@59847: (*##################################################################################
walther@59847: -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
walther@59847: 
walther@59847:   (*Aufgabe zum Einstieg in die Arbeit...*)
walther@60242:   val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
walther@59847:   (*ein 'ruleset' aus Poly.ML wird angewandt...*)
walther@59847:   val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
walther@59868:   UnparseC.term t;
walther@60242:   "a * b + (-1 * (a * x) + (-1 * (b * x) + x \<up> 2)) = 0";
walther@59847:   val SOME (t,_) = 
walther@59997:       rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
walther@59868:   UnparseC.term t;
walther@60242:   "x \<up> 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
walther@59847: (* bei Verwendung von "size_of-term" nach MG :*)
walther@60242: (*"x \<up> 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0"  !!! *)
walther@59847: 
walther@59847:   (*wir holen 'a' wieder aus der Klammerung heraus...*)
walther@59847:   val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
walther@59868:   UnparseC.term t;
walther@60242:    "x \<up> 2 + -1 * b * x + -1 * x * a + b * a = 0";
walther@60242: (* "x \<up> 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
walther@59847: 
walther@59847:   val SOME (t,_) =
walther@59997:       rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
walther@59868:   UnparseC.term t;
walther@60242:   "x \<up> 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; 
walther@59847:   (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
walther@60242:   "x \<up> 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
walther@59847: 
walther@59847:   (*das rewriting l"asst sich beobachten mit
walther@59901: Rewrite.trace_on := false;
walther@59847:   *)
walther@59847: 
walther@59847: "------15.11.02 --------------------------";
walther@60230:   val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
walther@60230:   val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
walther@60230:   val a = (Thm.term_of o the o (TermC.parse thy)) "a";
walther@59847:  
walther@59901: Rewrite.trace_on := false;
walther@59847:  (* Anwenden einer Regelmenge aus Termorder.ML: *)
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
walther@59868:  UnparseC.term t;
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_ thy false discard_parentheses t;
walther@59868:  UnparseC.term t;
walther@59847: "1 + b * x + x * a";
walther@59847: 
walther@60242:  val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
walther@59868:  UnparseC.term t;
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_ thy false discard_parentheses t;
walther@59868:  UnparseC.term t;
walther@60242: "1 + (x + b * x) * a + a \<up> 2";
walther@59847: 
walther@60242:  val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a  \<up> 2 * x + b * a + 7*a \<up> 2";
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
walther@59868:  UnparseC.term t;
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_ thy false discard_parentheses t;
walther@59868:  UnparseC.term t;
walther@60242: "1 + b * a + (7 + x) * a \<up> 2";
walther@59847: 
walther@59847: (* MG2003
walther@59847:  Prog_Expr.thy       grundlegende Algebra
walther@59847:  Poly.thy         Polynome
walther@59847:  Rational.thy     Br"uche
walther@59847:  Root.thy         Wurzeln
walther@59847:  RootRat.thy      Wurzen + Br"uche
walther@59847:  Termorder.thy    BITTE NUR HIERHER SCHREIBEN (...WN03)
walther@59847: 
walther@59847:  get_thm Termorder.thy "bdv_n_collect";
walther@59847:  get_thm (theory "Isac_Knowledge") "bdv_n_collect";
walther@59847: *)
walther@60242:  val t = (Thm.term_of o the o (TermC.parse thy)) "a  \<up> 2 * x + 7 * a \<up> 2";
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
walther@59868:  UnparseC.term t;
walther@59847:  val SOME (t,_) =
walther@59847:      rewrite_set_ thy false discard_parentheses t;
walther@59868:  UnparseC.term t;
walther@60242: "(7 + x) * a \<up> 2";
walther@59847: 
walther@60230:  val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
walther@59847: 
walther@59847:  val t = (Thm.term_of o the o (parseold thy)) "7";
walther@59847: ##################################################################################*)
walther@59847: 
walther@59847: 
walther@59847: "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
walther@59847: "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
walther@59847: "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
walther@60230:   val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
walther@60230:   val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
walther@60230:   val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
walther@59847: 
walther@60230:   val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
walther@60230:   val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
walther@60230:   val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
walther@60230:   val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
walther@59847: 
walther@59847: if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #1";
walther@59847:  
walther@59847: if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #2";
walther@59847: 
walther@59847: if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #3";
walther@59847: 
walther@60230:   val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
walther@60242:   val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
walther@59847:   ord_make_polynomial_in true thy substx (aa, bb);
walther@59847:   true; (* => LESS *) 
walther@59847:   
walther@60230:   val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
walther@60242:   val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
walther@59847:   ord_make_polynomial_in true thy substa (aa, bb);
walther@59847:   false; (* => GREATER *)
walther@59847: 
walther@59847: (* und nach dem Re-engineering der Termorders in den 'rulesets' 
walther@59847:    kannst Du die 'gr"osste' Variable frei w"ahlen: *)
walther@60230:   val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
walther@60230:   val x  = (Thm.term_of o the o (TermC.parse thy)) "x";
walther@60230:   val a  = (Thm.term_of o the o (TermC.parse thy)) "a";
walther@60230:   val b  = (Thm.term_of o the o (TermC.parse thy)) "b";
walther@59847: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
walther@59868: if UnparseC.term t' = "b + x + a" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #11";
walther@59847: 
walther@59847: val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
walther@59847: 
walther@59847: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
walther@59868: if UnparseC.term t' = "a + b + x" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #13";
walther@59847: 
walther@60242:   val ppp' = "-6 + -5*x + x \<up> 3 + -1*x \<up> 2 + -1*x \<up> 3 + -14*x \<up> 2";
walther@60230:   val ppp  = (Thm.term_of o the o (TermC.parse thy)) ppp';
walther@59847: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
walther@60242: if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #14";
walther@59847: 
walther@59847: val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
walther@60242: if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #15";
walther@59847: 
walther@59847:   val ttt' = "(3*x + 5)/18";
walther@60230:   val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
walther@59847: val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
walther@59868: if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
walther@59847: 
walther@59847: (*============ inhibit exn WN120316 ==============================================
walther@59847: val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
walther@59868: if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
walther@59847: else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
walther@59847: ============ inhibit exn WN120316 ==============================================*)
walther@59847: 
walther@59847: 
walther@59627: "----------- lin.eq degree_0 -------------------------------------";
walther@59627: "----------- lin.eq degree_0 -------------------------------------";
walther@59627: "----------- lin.eq degree_0 -------------------------------------";
walther@59627: "----- d0_false ------";
walther@59627: val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d0_polyeq_equation"]);
walther@59871: (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
walther@59627: TODO: change to "equality (x + -1*x = (0::real))"
walther@59627:       and search for an appropriate problem and method.
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
walther@59627: 
walther@59627: "----- d0_true ------";
walther@59997: val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d0_polyeq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
walther@59627: ============ inhibit exn WN110914 ============================================*)
walther@59627: 
walther@59627: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
walther@59627: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
walther@59627: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
walther@59627: "----- d2_pqformula1 ------!!!!";
walther@60242: val fmz = ["equality (-1/8 + (-1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
walther@59627: val (dI',pI',mI') =
walther@59997:   ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
walther@59627: 
walther@59627: (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
walther@59921: val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
walther@59921: val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
walther@59921: 
walther@59921: if p = ([], Res) andalso
walther@59921:   f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]" then
walther@60242:     case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
walther@60242: else error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
walther@59627: 
walther@60242: "----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
walther@60242: "----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
walther@60242: "----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
walther@59627: "----- d2_pqformula1_neg ------";
walther@60242: val fmz = ["equality (2 +(-1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: (*### or2list False
walther@59627:   ([1],Res)  False   Or_to_List)*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59627: (*### or2list False                           
walther@59627:   ([2],Res)  []      Check_elementwise "Assumptions"*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59844: val asm = Ctree.get_assumptions pt p;
walther@59627: if f2str f = "[]" andalso 
walther@60242:   UnparseC.terms asm = "[\"lhs (2 + -1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
walther@60242:     "\"lhs (2 + -1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
walther@60242: else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x \<up> 2 = 0";
walther@59627: 
walther@60242: "----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
walther@60242: "----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
walther@60242: "----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
walther@59627: "----- d2_pqformula2 ------";
walther@60242: val fmz = ["equality (-2 +(-1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 2, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
walther@59627: 
walther@59627: 
walther@60242: "----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
walther@60242: "----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
walther@60242: "----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
walther@59627: "----- d2_pqformula3 ------";
walther@59627: (*EP-9*)
walther@60242: val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59959: case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
walther@59627: 
walther@59627: 
walther@60242: "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
walther@59627: "----- d2_pqformula3_neg ------";
walther@60242: val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@59627: 
walther@60242: "----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
walther@60242: "----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
walther@60242: "----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
walther@59627: "----- d2_pqformula4 ------";
walther@60242: val fmz = ["equality (-2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
walther@60242: 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = -2]";
walther@59627: 
walther@60242: "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";
walther@59627: "----- d2_pqformula5 ------";
walther@60242: val fmz = ["equality (1*x +   x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@60242: "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
walther@60242: "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
walther@59627: "----- d2_pqformula6 ------";
walther@60242: val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@60242: "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";
walther@59627: "----- d2_pqformula7 ------";
walther@59627: (*EP-10*)
walther@60242: val fmz = ["equality (  x +   x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@60242: "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
walther@60242: "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
walther@59627: "----- d2_pqformula8 ------";
walther@60242: val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@60242: "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
walther@59627: "----- d2_pqformula9 ------";
walther@60242: val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
walther@59627: 
walther@59627: 
walther@60242: "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
walther@60242: "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
walther@59627: "----- d2_pqformula9_neg ------";
walther@60242: val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: "TODO 4 + 1*x \<up> 2 = 0";
walther@60242: "TODO 4 + 1*x \<up> 2 = 0";
walther@60242: "TODO 4 + 1*x \<up> 2 = 0";
walther@59627: 
walther@59627: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
walther@59627: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
walther@59627: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
walther@60242: val fmz = ["equality (-1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 1, x = -1 / 2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
walther@59627: 
walther@60242: "----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
walther@60242: "----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
walther@60242: "----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
walther@60242: val fmz = ["equality (1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: "TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
walther@60242: "TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
walther@60242: "TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
walther@59627: 
walther@59627: 
walther@60242: "----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
walther@60242: "----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
walther@60242: "----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
walther@59627: (*EP-11*)
walther@60242: val fmz = ["equality (-1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 1 / 2, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
walther@59627: 
walther@59627: 
walther@60242: "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
walther@60242: "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
walther@60242: "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
walther@60242: val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@60242: "TODO 1 + x + 2*x \<up> 2 = 0";
walther@60242: "TODO 1 + x + 2*x \<up> 2 = 0";
walther@60242: "TODO 1 + x + 2*x \<up> 2 = 0";
walther@59627: 
walther@59627: 
walther@60242: val fmz = ["equality (-2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
walther@59627: 
walther@60242: val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@60242: "TODO 2 + 1*x + x \<up> 2 = 0";
walther@60242: "TODO 2 + 1*x + x \<up> 2 = 0";
walther@60242: "TODO 2 + 1*x + x \<up> 2 = 0";
walther@59627: 
walther@59627: (*EP-12*)
walther@60242: val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
walther@59627: 
walther@60242: val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@60242: "TODO 2 + x + x \<up> 2 = 0";
walther@59627: 
walther@59627: (*EP-13*)
walther@60242: val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
walther@59627: 
walther@60242: val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: "TODO 8+ 2*x \<up> 2 = 0";
walther@60242: "TODO 8+ 2*x \<up> 2 = 0";
walther@60242: "TODO 8+ 2*x \<up> 2 = 0";
walther@59627: 
walther@59627: (*EP-14*)
walther@60242: val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
walther@59627: 
walther@59627: 
walther@60242: val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: "TODO 4+ x \<up> 2 = 0";
walther@60242: "TODO 4+ x \<up> 2 = 0";
walther@60242: "TODO 4+ x \<up> 2 = 0";
walther@59627: 
walther@59627: (*EP-15*)
walther@60242: val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@60242: val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@59627: (*EP-16*)
walther@60242: val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1 / 2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
walther@59627: 
walther@59627: (*EP-//*)
walther@60242: val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
walther@59997:                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59959: case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
walther@59627: 
walther@59627: 
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
walther@59627: (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
walther@59627: see --- val rls = calculate_RootRat > calculate_Rational ---
walther@59627: calculate_RootRat was a TODO with 2002, requires re-design.
walther@60242: see also --- (-8 - 2*x + x \<up> 2 = 0),  by rewriting --- below
walther@59627: *)
walther@60242:  val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
walther@59997:  	    "solveFor x", "solutions L"];
walther@59627:  val (dI',pI',mI') =
walther@59997:      ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
walther@59997:       ["PolyEq", "complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59997: (*Apply_Method ("PolyEq", "complete_square")*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
walther@60242:    2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
walther@60242:    -1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
walther@60242:    -1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
walther@60242:   x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
walther@60242:    x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
walther@60242:    NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up>  \<up> *)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: (*"x = -2 | x = 4" nxt = Or_to_List*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: (*"[x = -2, x = 4]" nxt = Check_Postcond*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
walther@59627: (* FIXXXME 
walther@59959:  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
walther@59627: *)
walther@59627: if f2str f =
walther@60242: "[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))]"
walther@60242: (*"[x = -1 * -1 + -1 * sqrt (1 \<up> 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 \<up> 2 - -8))]"*)
walther@59627: then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
walther@59627: 
walther@59627: 
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";
walther@60242: "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";
walther@59627: (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
walther@59627: see --- val rls = calculate_RootRat > calculate_Rational ---*)
walther@59627: val thy = @{theory PolyEq};
walther@59627: val ctxt = Proof_Context.init_global thy;
walther@59627: val inst = [((the o (parseNEW  ctxt)) "bdv::real", (the o (parseNEW  ctxt)) "x::real")];
walther@60242: val t = (the o (parseNEW  ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
walther@59627: 
walther@59627: val rls = complete_square;
walther@59627: val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
walther@60242: UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
walther@59627: 
walther@59871: val thm = ThmC.numerals_to_Free @{thm square_explicit1};
walther@59851: val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
walther@60242: UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
walther@59627: 
walther@59871: val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
walther@59627: val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
walther@60242: UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
walther@60242:            "\n2 / 2 - x = -1 * sqrt ((2 / 2) \<up> 2 - -8)";
walther@59627: 
walther@59627: (*the thm bdv_explicit2* here required to be constrained to ::real*)
walther@59871: val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
walther@59851: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
walther@60242: UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
walther@60242:               "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8)";
walther@59627: 
walther@59871: val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
walther@59851: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
walther@60242: UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
walther@60242:                    "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
walther@59627: 
walther@59871: val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
walther@59851: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
walther@60242: UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
walther@60242:                 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
walther@59627: 
walther@59627: val rls = calculate_RootRat;
walther@59627: val SOME (t,asm) = rewrite_set_ thy true rls t;
walther@59868: if UnparseC.term t =
walther@60242:   "-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))"
walther@60242: (*"-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*)
walther@60242: then () else error "(-8 - 2*x + x \<up> 2 = 0),  by rewriting -- ERROR INDICATES IMPROVEMENT";
walther@59868: (*SHOULD BE: UnparseC.term = "x = -2 | x = 4;*)
walther@59627: 
walther@59627: 
walther@60242: "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
walther@60242: "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
walther@60242: "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
walther@59627: "---- test the erls ----";
walther@60242:  val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
walther@59627:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
walther@59868:  val t' = UnparseC.term t;
wenzelm@60309:  (*if t'= \<^const_name>\<open>True\<close> then ()
walther@59627:  else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
walther@59627: (* *)
walther@60242:  val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
walther@59997:  	    "solveFor x", "solutions L"];
walther@59627:  val (dI',pI',mI') =
walther@59997:      ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
walther@59997:       ["PolyEq", "complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59997:  (*Apply_Method ("PolyEq", "complete_square")*)
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
walther@59627: 
walther@60242: "----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
walther@60242: "----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
walther@60242: "----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
walther@60242:  val fmz = ["equality (-16 + 4*x + 2*x \<up> 2 = 0)",
walther@59997:  	    "solveFor x", "solutions L"];
walther@59627:  val (dI',pI',mI') =
walther@59997:      ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
walther@59997:       ["PolyEq", "complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59997:  (*Apply_Method ("PolyEq", "complete_square")*)
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: (* FIXXXXME n1.,
walther@59959:  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
walther@59627: *)
walther@59627: