neuper@37906: (* testexamples for PolyEq, poynomial equations and equational systems
neuper@42248:    author: Richard Lang 2003  
neuper@37906:    (c) due to copyright terms
neuper@37906: WN030609: some expls dont work due to unfinished handling of 'expanded terms';
neuper@37906:           others marked with TODO have to be checked, too.
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@42319: (*WN060608 some ----- are not in this table.
neuper@42319:   WN111014.TODO missing checks*)
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- tests on predicates in problems ---------------------";
neuper@37906: "----------- test matching problems --------------------------0---";
neuper@42248: "----------- lin.eq degree_0 -------------------------------------";
neuper@42248: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906: "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
neuper@42318: "----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";
neuper@37906: "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
neuper@37906: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
neuper@37906: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
neuper@37906: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
neuper@37906: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
neuper@37906: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@42394: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@42394: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: "----------- tests on predicates in problems ---------------------";
neuper@37906: "----------- tests on predicates in problems ---------------------";
neuper@37906: "----------- tests on predicates in problems ---------------------";
neuper@37906: (* 
neuper@37906:  trace_rewrite:=true;
neuper@37906:  trace_rewrite:=false;
neuper@37906: *)
wneuper@59188:  val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
neuper@37906:  if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. in lhs";
neuper@37906: 
wneuper@59188:  val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 1 in is_expended_in";
neuper@37906: 
wneuper@59188:  val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
neuper@42248:  if (term2str t) = "False" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 2 in is_poly_in";
neuper@37906: 
wneuper@59188:  val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 3 in is_poly_in";
neuper@37906: 
wneuper@59188:  val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
neuper@37906: 
neuper@37906: 
wneuper@59188:  val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 5 in is_expended_in";
neuper@37906:  
wneuper@59188:  val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. in has_degree_in_in";
neuper@37906: 
wneuper@59188:  val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248:  if (term2str t) = "False" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
neuper@37906: 
wneuper@59188:  val t4 = (Thm.term_of o the o (parse thy)) 
neuper@37906: 	      "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248:  if (term2str t) = "False" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
neuper@37906: 
wneuper@59188:  val t5 = (Thm.term_of o the o (parse thy)) 
neuper@37906: 	      "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
neuper@42248:  if (term2str t) = "True" then ()
neuper@38031:  else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
neuper@37906: 
neuper@42248: "----------- test matching problems --------------------------0---";
neuper@42248: "----------- test matching problems --------------------------0---";
neuper@42248: "----------- test matching problems --------------------------0---";
neuper@42248: val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@42248: if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
neuper@42248:   Matches' {Find = [Correct "solutions L"], 
neuper@42248:             With = [], 
neuper@42248:             Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 
neuper@42248:             Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", 
neuper@42248:                      Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"], 
neuper@42248:             Relate = []}
neuper@42248: then () else error "match_pbl [expanded,univariate,equation]";
neuper@37906: 
neuper@42248: if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
neuper@42248:   Matches' {Find = [Correct "solutions L"], 
neuper@42248:             With = [], 
neuper@42248:             Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 
neuper@42248:             Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"], 
neuper@42248:             Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)
neuper@42248: then () else error "match_pbl [degree_2,expanded,univariate,equation]";
neuper@37906: 
neuper@42248: "----------- lin.eq degree_0 -------------------------------------";
neuper@42248: "----------- lin.eq degree_0 -------------------------------------";
neuper@42248: "----------- lin.eq degree_0 -------------------------------------";
neuper@37906: "----- d0_false ------";
neuper@42248: val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d0_polyeq_equation"]);
neuper@42283: (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
neuper@42283: TODO: change to "equality (x + -1*x = (0::real))"
neuper@42283:       and search for an appropriate problem and method.
neuper@42283: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
neuper@37906: 
neuper@37906: "----- d0_true ------";
neuper@42248: val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d0_polyeq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
neuper@42272: ============ inhibit exn WN110914 ============================================*)
neuper@37906: 
neuper@42248: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248: "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906: "----- d2_pqformula1 ------!!!!";
neuper@42255: val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
neuper@42255: val (dI',pI',mI') =
neuper@42255:   ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
neuper@42255: (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
neuper@42255: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
wneuper@59279: "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
neuper@42255: "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
neuper@42255: val (mI,m) = mk_tac'_ tac;
neuper@42255: val Appl m = applicable_in p pt m;
neuper@42255: val Check_elementwise' (trm1, str, (trm2, trms)) = m;
neuper@42255: term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255: str = "Assumptions";
neuper@42255: term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255: terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
neuper@42255:   "    (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
neuper@42255:   "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n     0) "^
neuper@42255:       "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
neuper@42255:   "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
neuper@42255:   "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
neuper@42255: (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
neuper@42255: member op = specsteps mI (*false*);
neuper@42255: (*loc_solve_ (mI,m) ptp;
neuper@42255:   WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255: "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
neuper@42255: (*solve m (pt, pos);
neuper@42255:   WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255: "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
neuper@42255: e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
neuper@42255:         val thy' = get_obj g_domID pt (par_pblobj pt p);
neuper@42255: 	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
neuper@42255: 		        val d = e_rls;
neuper@42255: (*locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
neuper@42255:   WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
wneuper@59279: "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
neuper@48790: 	                                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
neuper@42255:                                    ((thy',srls), m  ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
neuper@42255: val thy = assoc_thy thy';
neuper@42255: l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
neuper@42255: (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
neuper@42255:   ... Assoc ... is correct*)
neuper@48790: "~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
neuper@42387:    ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
neuper@42255: 1 < length l (*true*);
neuper@42255: val up = drop_last l;
neuper@42255:   term2str (go up sc);
neuper@42255:   (go up sc);
neuper@42255: (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
neuper@42255:       ... ???? ... is correct*)
neuper@48790: "~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
neuper@42255: 	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
neuper@42255:       val l = drop_last l; (*comes from e, goes to Abs*)
neuper@42255:       val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
neuper@42255:       val i = mk_Free (i, T);
neuper@42255:       val E = upd_env E (i, v);
neuper@42255: (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
wneuper@59279: val [(tac_, mout, ctree, pos', xxx)] = ss;
wneuper@59279: val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
neuper@42255: (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
neuper@42255:       ... Assoc ... is correct*)
neuper@42255: "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
neuper@42255:      ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
neuper@42255: val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
neuper@42255:              val ctxt = get_ctxt pt (p,p_)
neuper@42255:              val p' = lev_on p : pos;
neuper@42255: (* WAS val NotAss = assod pt d m stac
neuper@42255:       ... Ass ... is correct*)
neuper@42255: "~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
neuper@42255:     (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
neuper@42255: term2str consts;
neuper@42255: term2str consts';
neuper@42255: if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
neuper@42260: (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
neuper@37906: 
neuper@37906: "----- d2_pqformula1_neg ------";
neuper@42272: val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: (*### or2list False
neuper@37906:   ([1],Res)  False   Or_to_List)*)
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
neuper@37906: (*### or2list False
neuper@37906:   ([2],Res)  []      Check_elementwise "Assumptions"*)
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: val asm = get_assumptions_ pt p;
wneuper@59253: if f2str f = "[]" andalso 
neuper@42318:   terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
neuper@42318:     "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
neuper@38031: else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
neuper@37906: 
neuper@37906: "----- d2_pqformula2 ------";
neuper@37906: val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@42272: (*val p = e_pos'; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@42272: val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
neuper@37906: 
neuper@37906: 
neuper@37906: "----- d2_pqformula2_neg ------";
neuper@37906: val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
neuper@37906: "TODO 2 +(-1)*x + 1*x^^^2 = 0";
neuper@37906: "TODO 2 +(-1)*x + 1*x^^^2 = 0";
neuper@37906: "TODO 2 +(-1)*x + 1*x^^^2 = 0";
neuper@37906: 
neuper@37906: 
neuper@37906: "----- d2_pqformula3 ------";
neuper@37906: (*EP-9*)
neuper@37906: val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
wneuper@59267: case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
neuper@37906: 
neuper@37906: "----- d2_pqformula3_neg ------";
neuper@37906: val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: 
neuper@37906: 
neuper@37906: "----- d2_pqformula4 ------";
neuper@37906: val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
neuper@37906: 
neuper@37906: "----- d2_pqformula4_neg ------";
neuper@37906: val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 2 + x + 1*x^^^2 = 0";
neuper@37906: "TODO 2 + x + 1*x^^^2 = 0";
neuper@37906: "TODO 2 + x + 1*x^^^2 = 0";
neuper@37906: 
neuper@37906: "----- d2_pqformula5 ------";
neuper@37906: val fmz = ["equality (1*x +   x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: "----- d2_pqformula6 ------";
neuper@37906: val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: "----- d2_pqformula7 ------";
neuper@37906: (*EP-10*)
neuper@37906: val fmz = ["equality (  x +   x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: "----- d2_pqformula8 ------";
neuper@37906: val fmz = ["equality (  x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: "----- d2_pqformula9 ------";
neuper@37906: val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906: 
neuper@37906: 
neuper@37906: "----- d2_pqformula10_neg ------";
neuper@37906: val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 4 + x^^^2 = 0";
neuper@37906: "TODO 4 + x^^^2 = 0";
neuper@37906: "TODO 4 + x^^^2 = 0";
neuper@37906: 
neuper@37906: "----- d2_pqformula10 ------";
neuper@37906: val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906: 
neuper@37906: "----- d2_pqformula9_neg ------";
neuper@37906: val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 4 + 1*x^^^2 = 0";
neuper@37906: "TODO 4 + 1*x^^^2 = 0";
neuper@37906: "TODO 4 + 1*x^^^2 = 0";
neuper@37906: 
neuper@37906: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906: "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906: 
neuper@37906: val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 1, x = -1 / 2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
neuper@37906: 
neuper@37906: val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 1 +(-1)*x + 2*x^^^2 = 0";
neuper@37906: "TODO 1 +(-1)*x + 2*x^^^2 = 0";
neuper@37906: "TODO 1 +(-1)*x + 2*x^^^2 = 0";
neuper@37906: 
neuper@37906: (*EP-11*)
neuper@37906: val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 1 / 2, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
neuper@37906: 
neuper@37906: val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
neuper@37906: "TODO 1 + x + 2*x^^^2 = 0";
neuper@37906: "TODO 1 + x + 2*x^^^2 = 0";
neuper@37906: "TODO 1 + x + 2*x^^^2 = 0";
neuper@37906: 
neuper@37906: val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906: 
neuper@37906: val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
neuper@37906: "TODO 2 + 1*x + x^^^2 = 0";
neuper@37906: "TODO 2 + 1*x + x^^^2 = 0";
neuper@37906: "TODO 2 + 1*x + x^^^2 = 0";
neuper@37906: 
neuper@37906: (*EP-12*)
neuper@37906: val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906: 
neuper@37906: val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: "TODO 2 + x + x^^^2 = 0";
neuper@37906: 
neuper@37906: (*EP-13*)
neuper@37906: val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906: 
neuper@37906: val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 8+ 2*x^^^2 = 0";
neuper@37906: "TODO 8+ 2*x^^^2 = 0";
neuper@37906: "TODO 8+ 2*x^^^2 = 0";
neuper@37906: 
neuper@37906: (*EP-14*)
neuper@37906: val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906: 
neuper@37906: 
neuper@37906: val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: "TODO 4+ x^^^2 = 0";
neuper@37906: "TODO 4+ x^^^2 = 0";
neuper@37906: "TODO 4+ x^^^2 = 0";
neuper@37906: 
neuper@37906: (*EP-15*)
neuper@37906: val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: (*EP-16*)
neuper@37906: val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 0, x = -1 / 2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
neuper@37906: 
neuper@37906: (*EP-//*)
neuper@37906: val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906:                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267: case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906: 
neuper@37906: "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
neuper@37906: "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
neuper@37906: "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
neuper@42319: (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
neuper@42319: see --- val rls = calculate_RootRat > calculate_Rational ---
neuper@42319: calculate_RootRat was a TODO with 2002, requires re-design.
neuper@42319: see also --- (-8 - 2*x + x^^^2 = 0),  by rewriting --- below
neuper@42319: *)
neuper@37906:  val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991:  (*Apply_Method ("PolyEq","complete_square")*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
neuper@37906:     2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
neuper@37906:     -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
neuper@37906:     -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
neuper@37906:    x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
neuper@42319:     x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
neuper@42319:     NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"x = -2 | x = 4" nxt = Or_to_List*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906:  (*"[x = -2, x = 4]" nxt = Check_Postcond*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906: (* FIXXXME 
neuper@37906:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
neuper@37906: *)
neuper@52141: if f2str f =
neuper@52141: "[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
neuper@52141: (*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
neuper@52141: then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
neuper@37906: 
neuper@42318: "----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";
neuper@42318: "----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";
neuper@42318: "----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";
neuper@42319: (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
neuper@42319: see --- val rls = calculate_RootRat > calculate_Rational ---*)
neuper@42319: val thy = @{theory PolyEq};
neuper@48761: val ctxt = Proof_Context.init_global thy;
neuper@42319: val inst = [((the o (parseNEW  ctxt)) "bdv::real", (the o (parseNEW  ctxt)) "x::real")];
neuper@42319: val t = (the o (parseNEW  ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
neuper@42319: 
neuper@42319: val rls = complete_square;
neuper@42319: val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
neuper@42319: term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
neuper@42319: 
neuper@42319: val thm = num_str @{thm square_explicit1};
neuper@42319: val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
neuper@42319: term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
neuper@42319: 
neuper@42319: val thm = num_str @{thm root_plus_minus};
neuper@42319: val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
neuper@42319: term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
neuper@42319:            "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
neuper@42319: 
neuper@42319: (*the thm bdv_explicit2* here required to be constrained to ::real*)
neuper@42319: val thm = num_str @{thm bdv_explicit2};
neuper@42319: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319: term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
neuper@42319:               "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
neuper@42319: 
neuper@42319: val thm = num_str @{thm bdv_explicit3};
neuper@42319: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319: term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
neuper@42319:                    "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
neuper@42319: 
neuper@42319: val thm = num_str @{thm bdv_explicit2};
neuper@42319: val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319: term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
neuper@42319:                 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
neuper@42319: 
neuper@42319: val rls = calculate_RootRat;
neuper@42319: val SOME (t,asm) = rewrite_set_ thy true rls t;
neuper@52141: if term2str t = 
neuper@52141: "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
neuper@52141: (*"-1 * x = -1 + sqrt (1 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))"*)
neuper@42319: then () else error "(-8 - 2*x + x^^^2 = 0),  by rewriting -- ERROR INDICATES IMPROVEMENT";
neuper@42319: (*SHOULD BE: term2str = "x = -2 | x = 4;*)
neuper@42318: 
neuper@42318: 
neuper@37906: 
neuper@37906: "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
neuper@37906: "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
neuper@37906: "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
neuper@37906: "---- test the erls ----";
wneuper@59188:  val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
neuper@42319:  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
neuper@37906:  val t' = term2str t;
neuper@41928:  (*if t'= "HOL.True" then ()
neuper@38031:  else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
neuper@37906: (* *)
neuper@37906:  val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991:  (*Apply_Method ("PolyEq","complete_square")*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906: 
neuper@37906: "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
neuper@37906: "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
neuper@37906: "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
neuper@37906:  val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991:  (*Apply_Method ("PolyEq","complete_square")*)
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: (* FIXXXXME n1.,
neuper@37906:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
neuper@37906: *)
neuper@37906: 
neuper@37906: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
neuper@37906: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
neuper@37906: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
neuper@37906:  val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: 
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906: (*WN.2.5.03 TODO FIXME Matthias ?
neuper@37906:  case f of 
neuper@37906:      Form' 
neuper@37906: 	 (FormKF 
neuper@37906: 	      (~1,EdUndef,0,Nundef,
neuper@37906: 	       "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]")) 
neuper@37906: 	 => ()
neuper@38031:    | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
neuper@37906:  this will be simplified [x = a, x = b] to by Factor.ML*)
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
neuper@37906: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
neuper@37906: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
neuper@37906:  val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906: (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
neuper@37906:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
neuper@37906: *)
neuper@37906: 
neuper@37906: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
neuper@37906: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
neuper@37906: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
neuper@37906:  val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
neuper@37906:  	    "solveFor x","solutions L"];
neuper@37906:  val (dI',pI',mI') =
neuper@37991:      ("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906:       ["PolyEq","complete_square"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272:  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
neuper@37906:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
neuper@37906: *)
neuper@37906: if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
neuper@38031: else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
neuper@37906: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
neuper@37906: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
neuper@37906: (*EP-17 Schalk_I_p86_n5*)
neuper@42319: val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
neuper@37906: (* refine fmz ["univariate","equation"];
neuper@37906: *)
neuper@37991: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt =
neuper@37906:   ("Model_Problem",
neuper@37906:    Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906:   : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt =
neuper@37906:   ("Subproblem",
neuper@37991:    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906:   : string * tac *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt =
neuper@37906:   ("Model_Problem",
neuper@37906:    Model_Problem ["degree_1","polynomial","univariate","equation"])
neuper@37906:   : string * tac *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267: case f of FormKF "[x = 2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906: (*is in rlang.sml, too*)
neuper@37906: val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt =
neuper@37906:   ("Model_Problem",
neuper@37906:    Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906:   : string * tac *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt =
neuper@37906:   ("Subproblem",
neuper@37991:    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906:   : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt =
neuper@37906:   ("Model_Problem",
neuper@37906:    Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
neuper@37906:   : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267: case f of FormKF "[x = 2 / 15, x = 1]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
neuper@37906: 
neuper@37906: 
neuper@37906: "    -4 + x^^^2 =0     ";
neuper@37906: "    -4 + x^^^2 =0     ";
neuper@37906: "    -4 + x^^^2 =0     ";
neuper@37906: val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
neuper@37906: (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
neuper@37906: (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
neuper@37991: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906: (*val p = e_pos'; 
neuper@37906: val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267: case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
neuper@37906: 
neuper@37906: "----------------- polyeq.sml end ------------------";
neuper@37906: 
neuper@37906: (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
neuper@37906: (*WN.19.3.03 ---v-*)
neuper@37906: (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
neuper@37906: val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
neuper@37926: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906: term2str t';
neuper@37906: "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
neuper@37906: (*WN.19.3.03 ---^-*)
neuper@37906: 
neuper@37906: (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
neuper@37906: val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
neuper@37926: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906: term2str t';
neuper@37906: "y ^^^ 2 + -2 * x * p = 0";
neuper@37906: 
neuper@37906: (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
neuper@37906: val t = str2term 
neuper@37906: "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
neuper@37926: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906: term2str t';
neuper@37906: "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
neuper@37926: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
neuper@37906: term2str t';
neuper@37906: "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
neuper@37906: 
neuper@37906: (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
neuper@37906: val t = str2term 
neuper@37906: "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
neuper@37926: val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906: (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
neuper@37906: 
neuper@37906: 
neuper@37906: val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
neuper@37906: trace_rewrite:=true;
neuper@37906: rewrite_set_ thy false expand_binoms t;
neuper@37906: trace_rewrite:=false;
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
s1210629013@55445: reset_states ();
neuper@37906: CalcTree
neuper@42319: [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], 
neuper@37991:   ("PolyEq",["univariate","equation"],["no_met"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@42394: interSteps 1 ([1],Res)
neuper@42394: (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
neuper@37906: 
neuper@42394: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394: val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
neuper@42394: val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
neuper@42394: val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
neuper@42394: (* steps in rls d2_polyeq_bdv_only_simplify:*)
neuper@42248: 
neuper@42394: (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(bdv,x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
neuper@42394: t |> term2str; t |> atomty;
neuper@42394: val thm = num_str @{thm d2_prescind1};
wneuper@59188: thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
neuper@42394: val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
neuper@42394: 
neuper@42394: (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(bdv,x)"],("d2_reduce_equation1","")) 
neuper@42394:                                                                         --> x = 0 | -6 + 5 * x = 0*)
neuper@42394: t' |> term2str; t' |> atomty;
neuper@42394: val thm = num_str @{thm d2_reduce_equation1};
wneuper@59188: thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
neuper@42394: val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t'';
neuper@42394: (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
neuper@42394:    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
neuper@42394: *)
neuper@42394: if term2str t'' = "x = 0 | -6 + 5 * x = 0" then ()
neuper@42394: else error "rls d2_polyeq_bdv_only_simplify broken";
neuper@42394: 
neuper@42394: