wneuper/isa: test/Tools/isac/Knowledge/polyeq.sml@255c853ea2f0 (annotated)

neuper@37906	1	(* testexamples for PolyEq, poynomial equations and equational systems
neuper@42248	2	author: Richard Lang 2003
neuper@37906	3	(c) due to copyright terms
neuper@37906	4	WN030609: some expls dont work due to unfinished handling of 'expanded terms';
neuper@37906	5	others marked with TODO have to be checked, too.
neuper@37906	6	*)
neuper@37906	7
neuper@37906	8	"-----------------------------------------------------------------";
neuper@37906	9	"table of contents -----------------------------------------------";
neuper@42319	10	(*WN060608 some ----- are not in this table.
neuper@42319	11	WN111014.TODO missing checks*)
neuper@37906	12	"-----------------------------------------------------------------";
neuper@37906	13	"----------- tests on predicates in problems ---------------------";
neuper@37906	14	"----------- test matching problems --------------------------0---";
neuper@42248	15	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	16	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906	17	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@42318	18	"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
neuper@37906	19	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	20	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	21	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	22	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	23	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	24	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	25	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@42394	26	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@42394	27	"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@37906	28	"-----------------------------------------------------------------";
neuper@37906	29	"-----------------------------------------------------------------";
neuper@37906	30
neuper@37906	31	"----------- tests on predicates in problems ---------------------";
neuper@37906	32	"----------- tests on predicates in problems ---------------------";
neuper@37906	33	"----------- tests on predicates in problems ---------------------";
neuper@37906	34	(*
neuper@37906	35	trace_rewrite:=true;
neuper@37906	36	trace_rewrite:=false;
neuper@37906	37	*)
wneuper@59188	38	val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
neuper@42248	39	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
neuper@37906	40	if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
neuper@38031	41	else error "polyeq.sml: diff.behav. in lhs";
neuper@37906	42
wneuper@59188	43	val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
neuper@42248	44	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
neuper@42248	45	if (term2str t) = "True" then ()
neuper@38031	46	else error "polyeq.sml: diff.behav. 1 in is_expended_in";
neuper@37906	47
wneuper@59188	48	val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
neuper@42248	49	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
neuper@42248	50	if (term2str t) = "False" then ()
neuper@38031	51	else error "polyeq.sml: diff.behav. 2 in is_poly_in";
neuper@37906	52
wneuper@59188	53	val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)2x + x^^^2) is_poly_in x";
neuper@42248	54	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	55	if (term2str t) = "True" then ()
neuper@38031	56	else error "polyeq.sml: diff.behav. 3 in is_poly_in";
neuper@37906	57
wneuper@59188	58	val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)2x + x^^^2 = 0)) is_expanded_in x";
neuper@42248	59	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248	60	if (term2str t) = "True" then ()
neuper@38031	61	else error "polyeq.sml: diff.behav. 4 in is_expended_in";
neuper@37906	62
neuper@37906	63
wneuper@59188	64	val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
neuper@42248	65	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
neuper@42248	66	if (term2str t) = "True" then ()
neuper@38031	67	else error "polyeq.sml: diff.behav. 5 in is_expended_in";
neuper@37906	68
wneuper@59188	69	val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248	70	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	71	if (term2str t) = "True" then ()
neuper@38031	72	else error "polyeq.sml: diff.behav. in has_degree_in_in";
neuper@37906	73
wneuper@59188	74	val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
neuper@42248	75	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	76	if (term2str t) = "False" then ()
neuper@38031	77	else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
neuper@37906	78
wneuper@59188	79	val t4 = (Thm.term_of o the o (parse thy))
neuper@37906	80	"((-8 - 2*x + x^^^2) has_degree_in x) = 1";
neuper@42248	81	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248	82	if (term2str t) = "False" then ()
neuper@38031	83	else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
neuper@37906	84
wneuper@59188	85	val t5 = (Thm.term_of o the o (parse thy))
neuper@37906	86	"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248	87	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
neuper@42248	88	if (term2str t) = "True" then ()
neuper@38031	89	else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
neuper@37906	90
neuper@42248	91	"----------- test matching problems --------------------------0---";
neuper@42248	92	"----------- test matching problems --------------------------0---";
neuper@42248	93	"----------- test matching problems --------------------------0---";
neuper@42248	94	val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@42248	95	if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
neuper@42248	96	Matches' {Find = [Correct "solutions L"],
neuper@42248	97	With = [],
neuper@42248	98	Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
neuper@42248	99	Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
neuper@42248	100	Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
neuper@42248	101	Relate = []}
neuper@42248	102	then () else error "match_pbl [expanded,univariate,equation]";
neuper@37906	103
neuper@42248	104	if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
neuper@42248	105	Matches' {Find = [Correct "solutions L"],
neuper@42248	106	With = [],
neuper@42248	107	Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
neuper@42248	108	Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
neuper@42248	109	Relate = []} (before WN110906 was: has_degree_in x =!= 2"])
neuper@42248	110	then () else error "match_pbl [degree_2,expanded,univariate,equation]";
neuper@37906	111
neuper@42248	112	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	113	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	114	"----------- lin.eq degree_0 -------------------------------------";
neuper@37906	115	"----- d0_false ------";
neuper@42248	116	val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
neuper@37991	117	val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906	118	["PolyEq","solve_d0_polyeq_equation"]);
neuper@42283	119	(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
neuper@42283	120	TODO: change to "equality (x + -1*x = (0::real))"
neuper@42283	121	and search for an appropriate problem and method.
neuper@42283	122
neuper@37906	123	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	124	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	125	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	126	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	127	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	128	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	129	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	130	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
neuper@38031	131	\| _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
neuper@37906	132
neuper@37906	133	"----- d0_true ------";
neuper@42248	134	val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
neuper@37991	135	val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906	136	["PolyEq","solve_d0_polyeq_equation"]);
neuper@37906	137	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	138	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	139	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	140	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	141	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	142	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	143	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	144	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
neuper@38031	145	\| _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
neuper@42272	146	============ inhibit exn WN110914 ============================================*)
neuper@37906	147
neuper@42248	148	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248	149	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248	150	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906	151	"----- d2_pqformula1 ------!!!!";
neuper@42255	152	val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
neuper@42255	153	val (dI',pI',mI') =
neuper@42255	154	("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
neuper@37906	155	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42255	156	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	157	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	158	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	159	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	160	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	161	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	162	val (p,_,f,nxt,_,pt) = me nxt p [] pt; (Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"])
neuper@42255	163	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	164	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	165	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	166	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	167	([z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 sqrt (9 / 16) / 2] TODO sqrt*)
neuper@42255	168	val (p,_,f,nxt,_,pt) = me nxt p [] pt; (nxt =..,Check_elementwise "Assumptions"))
wneuper@59279	169	"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
neuper@42255	170	"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
neuper@42255	171	val (mI,m) = mk_tac'_ tac;
neuper@42255	172	val Appl m = applicable_in p pt m;
neuper@42255	173	val Check_elementwise' (trm1, str, (trm2, trms)) = m;
neuper@42255	174	term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255	175	str = "Assumptions";
neuper@42255	176	term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255	177	terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
neuper@42255	178	" (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
neuper@42255	179	"\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
neuper@42255	180	"has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
neuper@42255	181	"\"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	182	"\"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	183	(TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in);
neuper@42255	184	member op = specsteps mI (false);
neuper@42255	185	(*loc_solve_ (mI,m) ptp;
neuper@42255	186	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255	187	"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
neuper@42255	188	(*solve m (pt, pos);
neuper@42255	189	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255	190	"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
neuper@42255	191	e_metID = get_obj g_metID pt (par_pblobj pt p) (false);
neuper@42255	192	val thy' = get_obj g_domID pt (par_pblobj pt p);
neuper@42255	193	val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
neuper@42255	194	val d = e_rls;
neuper@42255	195	(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
neuper@42255	196	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
wneuper@59279	197	"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
neuper@48790	198	(scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
neuper@42255	199	((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
neuper@42255	200	val thy = assoc_thy thy';
neuper@42255	201	l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (false);
neuper@42255	202	(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
neuper@42255	203	... Assoc ... is correct*)
neuper@48790	204	"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
neuper@42387	205	((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
neuper@42255	206	1 < length l (true);
neuper@42255	207	val up = drop_last l;
neuper@42255	208	term2str (go up sc);
neuper@42255	209	(go up sc);
neuper@42255	210	(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
neuper@42255	211	... ???? ... is correct*)
neuper@48790	212	"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
neuper@42255	213	(Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
neuper@42255	214	val l = drop_last l; (comes from e, goes to Abs)
neuper@42255	215	val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
neuper@42255	216	val i = mk_Free (i, T);
neuper@42255	217	val E = upd_env E (i, v);
neuper@42255	218	(Type error ...: Can't unify _a to pos pos_ (Incompatible types)*)
wneuper@59279	219	val [(tac_, mout, ctree, pos', xxx)] = ss;
wneuper@59279	220	val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
neuper@42255	221	(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
neuper@42255	222	... Assoc ... is correct*)
neuper@42255	223	"~~~~~ 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	224	((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
neuper@42255	225	val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
neuper@42255	226	val ctxt = get_ctxt pt (p,p_)
neuper@42255	227	val p' = lev_on p : pos;
neuper@42255	228	(* WAS val NotAss = assod pt d m stac
neuper@42255	229	... Ass ... is correct*)
neuper@42255	230	"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
neuper@42255	231	(Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
neuper@42255	232	term2str consts;
neuper@42255	233	term2str consts';
neuper@42255	234	if consts = consts' (WAS false) then () else error "Check_elementwise changed";
neuper@42260	235	([z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 sqrt (9 / 16) / 2] TODO sqrt*)
neuper@37906	236
neuper@37906	237	"----- d2_pqformula1_neg ------";
neuper@42272	238	val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
neuper@37991	239	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	240	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	241	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	242	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	243	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	244	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	245	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	246	(*### or2list False
neuper@37906	247	([1],Res) False Or_to_List)*)
neuper@42272	248	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	249	(*### or2list False
neuper@37906	250	([2],Res) [] Check_elementwise "Assumptions"*)
neuper@42272	251	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	252	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	253	val asm = get_assumptions_ pt p;
wneuper@59253	254	if f2str f = "[]" andalso
neuper@42318	255	terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
neuper@42318	256	"\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
neuper@38031	257	else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
neuper@37906	258
neuper@37906	259	"----- d2_pqformula2 ------";
neuper@37906	260	val fmz = ["equality (-2 +(-1)x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	261	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	262	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@42272	263	(*val p = e_pos';
neuper@37906	264	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@42272	265	val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
neuper@37906	266	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	267	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	268	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	269	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	270	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	271	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	272	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	273	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	274	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	275	case f of FormKF "[x = 2, x = -1]" => ()
neuper@38031	276	\| _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
neuper@37906	277
neuper@37906	278
neuper@37906	279	"----- d2_pqformula2_neg ------";
neuper@37906	280	val fmz = ["equality ( 2 +(-1)x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	281	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	282	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	283	(*val p = e_pos'; val c = [];
neuper@37906	284	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	285	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	286	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	287	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	288	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	289	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	290	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	291	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	292	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	293	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	294	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	295	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	296	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	297
neuper@37906	298
neuper@37906	299	"----- d2_pqformula3 ------";
neuper@37906	300	(EP-9)
neuper@37906	301	val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	302	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	303	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	304	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	305	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	306	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	307	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	308	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	309	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	310	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	311	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	312	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	313	case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031	314	\| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
neuper@37906	315
neuper@37906	316	"----- d2_pqformula3_neg ------";
neuper@37906	317	val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	318	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	319	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	320	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	321	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	322	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	323	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	324	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	325	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	326	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	327	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	328	"TODO 2 + x + x^^^2 = 0";
neuper@37906	329	"TODO 2 + x + x^^^2 = 0";
neuper@37906	330	"TODO 2 + x + x^^^2 = 0";
neuper@37906	331
neuper@37906	332
neuper@37906	333	"----- d2_pqformula4 ------";
neuper@37906	334	val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	335	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	336	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	337	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	338	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	339	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	340	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	341	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	342	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	343	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	344	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	345	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	346	case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031	347	\| _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
neuper@37906	348
neuper@37906	349	"----- d2_pqformula4_neg ------";
neuper@37906	350	val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	351	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	352	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	353	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	354	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	355	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	356	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	357	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	358	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	359	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	360	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	361	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	362	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	363
neuper@37906	364	"----- d2_pqformula5 ------";
neuper@37906	365	val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	366	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	367	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	368	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	369	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	370	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	371	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	372	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	373	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	374	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	375	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	376	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	377	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	378	\| _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	379
neuper@37906	380	"----- d2_pqformula6 ------";
neuper@37906	381	val fmz = ["equality (1x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	382	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	383	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	384	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	385	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	386	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	387	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	388	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	389	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	390	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	391	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	392	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	393	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	394	\| _ => error "polyeq.sml: diff.behav. in 1x + 1x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	395
neuper@37906	396	"----- d2_pqformula7 ------";
neuper@37906	397	(EP-10)
neuper@37906	398	val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	399	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	400	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	401	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	402	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	403	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	404	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	405	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	406	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	407	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	408	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	409	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	410	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	411	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	412
neuper@37906	413	"----- d2_pqformula8 ------";
neuper@37906	414	val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	415	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	416	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	417	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	418	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	419	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	420	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	421	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	422	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	423	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	424	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	425	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	426	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	427	\| _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	428
neuper@37906	429	"----- d2_pqformula9 ------";
neuper@37906	430	val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	431	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	432	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	433	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	434	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	435	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	436	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	437	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	438	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	439	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	440	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	441	case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031	442	\| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	443
neuper@37906	444
neuper@37906	445	"----- d2_pqformula10_neg ------";
neuper@37906	446	val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	447	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	448	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	449	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	450	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	451	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	452	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	453	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	454	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	455	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	456	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	457	"TODO 4 + x^^^2 = 0";
neuper@37906	458	"TODO 4 + x^^^2 = 0";
neuper@37906	459	"TODO 4 + x^^^2 = 0";
neuper@37906	460
neuper@37906	461	"----- d2_pqformula10 ------";
neuper@37906	462	val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	463	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	464	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	465	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	466	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	467	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	468	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	469	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	470	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	471	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	472	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	473	case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031	474	\| _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	475
neuper@37906	476	"----- d2_pqformula9_neg ------";
neuper@37906	477	val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	478	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	479	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	480	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	481	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	482	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	483	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	484	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	485	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	486	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	487	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	488	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	489	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	490
neuper@37906	491	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	492	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	493	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	494
neuper@37906	495	val fmz = ["equality (-1 +(-1)x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	496	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	497	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	498	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	499	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	500	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	501	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	502	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	503	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	504	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	505	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	506	case f of FormKF "[x = 1, x = -1 / 2]" => ()
neuper@38031	507	\| _ => error "polyeq.sml: diff.behav. in -1 + (-1)x + 2x^2 = 0 -> [x = 1, x = -1/2]";
neuper@37906	508
neuper@37906	509	val fmz = ["equality ( 1 +(-1)x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	510	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	511	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	512	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	513	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	514	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	515	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	516	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	517	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	518	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	519	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	520	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	521	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	522
neuper@37906	523	(EP-11)
neuper@37906	524	val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	525	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	526	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	527	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	528	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	529	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	530	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	531	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	532	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	533	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	534	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	535	case f of FormKF "[x = 1 / 2, x = -1]" => ()
neuper@38031	536	\| _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
neuper@37906	537
neuper@37906	538	val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	539	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	540	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	541	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	542	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	543	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	544	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	545	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	546	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	547	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	548	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	549	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	550	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	551	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	552
neuper@37906	553	val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	554	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	555	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	556	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	557	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	558	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	559	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	560	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	561	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	562	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	563	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	564	case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031	565	\| _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906	566
neuper@37906	567	val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	568	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	569	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	570	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	571	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	572	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	573	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	574	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	575	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	576	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	577	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	578	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	579	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	580	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	581
neuper@37906	582	(EP-12)
neuper@37906	583	val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	584	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	585	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	586	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	587	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	588	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	589	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	590	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	591	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	592	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	593	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	594	case f of FormKF "[x = 1, x = -2]" => ()
neuper@38031	595	\| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906	596
neuper@37906	597	val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	598	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	599	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	600	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	601	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	602	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	603	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	604	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	605	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	606	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	607	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	608	"TODO 2 + x + x^^^2 = 0";
neuper@37906	609	"TODO 2 + x + x^^^2 = 0";
neuper@37906	610	"TODO 2 + x + x^^^2 = 0";
neuper@37906	611
neuper@37906	612	(EP-13)
neuper@37906	613	val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	614	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	615	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	616	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	617	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	618	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	619	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	620	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	621	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	622	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	623	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	624	case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031	625	\| _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	626
neuper@37906	627	val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	628	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	629	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	630	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	631	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	632	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	633	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	634	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	635	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	636	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	637	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	638	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	639	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	640
neuper@37906	641	(EP-14)
neuper@37906	642	val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	643	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	644	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	645	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	646	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	647	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	648	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	649	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	650	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	651	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	652	case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031	653	\| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	654
neuper@37906	655
neuper@37906	656	val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	657	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	658	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	659	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	660	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	661	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	662	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	663	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	664	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	665	"TODO 4+ x^^^2 = 0";
neuper@37906	666	"TODO 4+ x^^^2 = 0";
neuper@37906	667	"TODO 4+ x^^^2 = 0";
neuper@37906	668
neuper@37906	669	(EP-15)
neuper@37906	670	val fmz = ["equality (2x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	671	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	672	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	673	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	674	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	675	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	676	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	677	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	678	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	679	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	680	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	681	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	682	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	683
neuper@37906	684	val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	685	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	686	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	687	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	688	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	689	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	690	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	691	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	692	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	693	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	694	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	695	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	696	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	697
neuper@37906	698	(EP-16)
neuper@37906	699	val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	700	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	701	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	702	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	703	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	704	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	705	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	706	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	707	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	708	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	709	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	710	case f of FormKF "[x = 0, x = -1 / 2]" => ()
neuper@38031	711	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
neuper@37906	712
neuper@37906	713	(EP-//)
neuper@37906	714	val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	715	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	716	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	717	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	718	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	719	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	720	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	721	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	722	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	723	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	724	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59267	725	case f of FormKF "[x = 0, x = -1]" => ()
neuper@38031	726	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	727
neuper@37906	728	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	729	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	730	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@42319	731	(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
neuper@42319	732	see --- val rls = calculate_RootRat > calculate_Rational ---
neuper@42319	733	calculate_RootRat was a TODO with 2002, requires re-design.
neuper@42319	734	see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
neuper@42319	735	*)
neuper@37906	736	val fmz = ["equality (-8 - 2x + x^^^2 = 0)", (Schalk 2, S.67 Nr.31.b*)
neuper@37906	737	"solveFor x","solutions L"];
neuper@37906	738	val (dI',pI',mI') =
neuper@37991	739	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	740	["PolyEq","complete_square"]);
neuper@37906	741	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	742	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	743	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	744	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	745	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	746	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	747	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	748	("-8 - 2 x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
neuper@42272	749	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	750	("-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1")
neuper@42272	751	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	752	("(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus)
neuper@42272	753	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	754	(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	755	2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
neuper@42272	756	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	757	(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	758	-1x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2")
neuper@42272	759	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	760	("-1 x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	761	-1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
neuper@42272	762	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	763	("-1 x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	764	x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
neuper@42272	765	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	766	("x = -1 (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) \|
neuper@42319	767	x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
neuper@42319	768	NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
neuper@42272	769	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	770	("x = -2 \| x = 4" nxt = Or_to_List)
neuper@42272	771	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	772	("[x = -2, x = 4]" nxt = Check_Postcond)
neuper@42272	773	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	774	(* FIXXXME
neuper@37906	775	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
neuper@38031	776	\| _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
neuper@37906	777	*)
neuper@52141	778	if f2str f =
neuper@52141	779	"[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
neuper@52141	780	("[x = -1 -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
neuper@52141	781	then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
neuper@37906	782
neuper@42318	783	"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
neuper@42318	784	"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
neuper@42318	785	"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
neuper@42319	786	(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
neuper@42319	787	see --- val rls = calculate_RootRat > calculate_Rational ---*)
neuper@42319	788	val thy = @{theory PolyEq};
neuper@48761	789	val ctxt = Proof_Context.init_global thy;
neuper@42319	790	val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
neuper@42319	791	val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
neuper@42319	792
neuper@42319	793	val rls = complete_square;
neuper@42319	794	val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
neuper@42319	795	term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
neuper@42319	796
neuper@42319	797	val thm = num_str @{thm square_explicit1};
neuper@42319	798	val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
neuper@42319	799	term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
neuper@42319	800
neuper@42319	801	val thm = num_str @{thm root_plus_minus};
neuper@42319	802	val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
neuper@42319	803	term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|"^
neuper@42319	804	"\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
neuper@42319	805
neuper@42319	806	(the thm bdv_explicit2 here required to be constrained to ::real*)
neuper@42319	807	val thm = num_str @{thm bdv_explicit2};
neuper@42319	808	val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319	809	term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|"^
neuper@42319	810	"\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
neuper@42319	811
neuper@42319	812	val thm = num_str @{thm bdv_explicit3};
neuper@42319	813	val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319	814	term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|"^
neuper@42319	815	"\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
neuper@42319	816
neuper@42319	817	val thm = num_str @{thm bdv_explicit2};
neuper@42319	818	val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
neuper@42319	819	term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) \|"^
neuper@42319	820	"\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
neuper@42319	821
neuper@42319	822	val rls = calculate_RootRat;
neuper@42319	823	val SOME (t,asm) = rewrite_set_ thy true rls t;
neuper@52141	824	if term2str t =
neuper@52141	825	"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \|\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
neuper@52141	826	("-1 x = -1 + sqrt (1 ^^^ 2 - -8) \|\nx = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))"*)
neuper@42319	827	then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
neuper@42319	828	(SHOULD BE: term2str = "x = -2 \| x = 4;)
neuper@42318	829
neuper@42318	830
neuper@37906	831
neuper@37906	832	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	833	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	834	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	835	"---- test the erls ----";
wneuper@59188	836	val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
neuper@42319	837	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
neuper@37906	838	val t' = term2str t;
neuper@41928	839	(*if t'= "HOL.True" then ()
neuper@38031	840	else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
neuper@37906	841	(* *)
neuper@37906	842	val fmz = ["equality (3 - 10x + 3x^^^2 = 0)",
neuper@37906	843	"solveFor x","solutions L"];
neuper@37906	844	val (dI',pI',mI') =
neuper@37991	845	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	846	["PolyEq","complete_square"]);
neuper@37906	847	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	848	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	849	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	850	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	851	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	852	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	853	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	854	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	855	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	856	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	857
neuper@37906	858	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	859	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	860	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	861	val fmz = ["equality (-16 + 4x + 2x^^^2 = 0)",
neuper@37906	862	"solveFor x","solutions L"];
neuper@37906	863	val (dI',pI',mI') =
neuper@37991	864	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	865	["PolyEq","complete_square"]);
neuper@37906	866	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	867	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	868	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	869	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	870	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	871	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	872	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	873	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	874	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	875	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	876	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	877	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	878	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	879	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	880	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	881	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	882	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	883	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	884	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	885	(* FIXXXXME n1.,
neuper@37906	886	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
neuper@38031	887	\| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
neuper@37906	888	*)
neuper@37906	889
neuper@37906	890	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	891	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	892	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	893	val fmz = ["equality (ab - (a+b)x + x^^^2 = 0)",
neuper@37906	894	"solveFor x","solutions L"];
neuper@37906	895	val (dI',pI',mI') =
neuper@37991	896	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	897	["PolyEq","complete_square"]);
neuper@37906	898	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	899	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	900	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	901	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	902	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	903	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	904	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	905	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	906	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	907	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	908	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	909
neuper@42272	910	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	911	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	912	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	913	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	914	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	915	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	916	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	917	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	918	(*WN.2.5.03 TODO FIXME Matthias ?
neuper@37906	919	case f of
neuper@37906	920	Form'
neuper@37906	921	(FormKF
neuper@37906	922	(~1,EdUndef,0,Nundef,
neuper@37906	923	"[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	924	=> ()
neuper@38031	925	\| _ => error "polyeq.sml: diff.behav. in ab - (a+b)x + x^^^2 = 0";
neuper@37906	926	this will be simplified [x = a, x = b] to by Factor.ML*)
neuper@37906	927
neuper@37906	928
neuper@37906	929	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	930	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	931	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	932	val fmz = ["equality (-64 + x^^^2 = 0)",(Schalk 2, S.66 Nr.1.a~)
neuper@37906	933	"solveFor x","solutions L"];
neuper@37906	934	val (dI',pI',mI') =
neuper@37991	935	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	936	["PolyEq","complete_square"]);
neuper@37906	937	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	938	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	939	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	940	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	941	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	942	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	943	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	944	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	945	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	946	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	947	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	948	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	949	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	950	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	951	(WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 sqrt (0 - -64)]"
neuper@37906	952	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
neuper@38031	953	\| _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
neuper@37906	954	*)
neuper@37906	955
neuper@37906	956	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	957	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	958	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	959	val fmz = ["equality (-147 + 3x^^^2 = 0)",(Schalk 2, S.66 Nr.1.b*)
neuper@37906	960	"solveFor x","solutions L"];
neuper@37906	961	val (dI',pI',mI') =
neuper@37991	962	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	963	["PolyEq","complete_square"]);
neuper@37906	964	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	965	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	966	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	967	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	968	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	969	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	970	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	971	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	972	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	973	(WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 sqrt (0 - -49)]"
neuper@37906	974	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
neuper@38031	975	\| _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
neuper@37906	976	*)
neuper@37906	977	if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
neuper@38031	978	else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
neuper@37906	979
neuper@37906	980
neuper@37906	981	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	982	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	983	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	984	(EP-17 Schalk_I_p86_n5)
neuper@42319	985	val fmz = ["equality ((3::real)x - 1 - (5x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
neuper@37906	986	(* refine fmz ["univariate","equation"];
neuper@37906	987	*)
neuper@37991	988	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	989	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	990	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	991	(* val nxt =
neuper@37906	992	("Model_Problem",
neuper@37906	993	Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906	994	: string * tac*)
neuper@37906	995	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	996	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	997	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	998	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	999	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1000	(* val nxt =
neuper@37906	1001	("Subproblem",
neuper@37991	1002	Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906	1003	: string * tac *)
neuper@37906	1004	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1005	(*val nxt =
neuper@37906	1006	("Model_Problem",
neuper@37906	1007	Model_Problem ["degree_1","polynomial","univariate","equation"])
neuper@37906	1008	: string * tac *)
neuper@37906	1009	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1010	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1011
neuper@37906	1012	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1013	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1014	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1015	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1016	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267	1017	case f of FormKF "[x = 2]" => ()
neuper@38031	1018	\| _ => error "polyeq.sml: diff.behav. in [x = 2]";
neuper@37906	1019
neuper@37906	1020
neuper@37906	1021	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1022	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1023	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1024	(is in rlang.sml, too)
neuper@37906	1025	val fmz = ["equality ((x+1)(x+2) - (3x - 2)^^^2=(2x - 1)^^^2+(3x - 1)*(x+1))",
neuper@37906	1026	"solveFor x","solutions L"];
neuper@37991	1027	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	1028	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	1029	(val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]))
neuper@37906	1030	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1031	(* val nxt =
neuper@37906	1032	("Model_Problem",
neuper@37906	1033	Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906	1034	: string * tac *)
neuper@37906	1035	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1036	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1037	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1038	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1039	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1040	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1041	(* val nxt =
neuper@37906	1042	("Subproblem",
neuper@37991	1043	Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906	1044	: string * tac*)
neuper@37906	1045	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1046	(*val nxt =
neuper@37906	1047	("Model_Problem",
neuper@37906	1048	Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
neuper@37906	1049	: string * tac*)
neuper@37906	1050	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1051	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1052	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1053	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1054	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1055	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1056	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267	1057	case f of FormKF "[x = 2 / 15, x = 1]" => ()
neuper@38031	1058	\| _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
neuper@37906	1059
neuper@37906	1060
neuper@37906	1061	" -4 + x^^^2 =0 ";
neuper@37906	1062	" -4 + x^^^2 =0 ";
neuper@37906	1063	" -4 + x^^^2 =0 ";
neuper@37906	1064	val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
neuper@37906	1065	(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
neuper@37906	1066	(val fmz = ["equality (0 =0)", "solveFor x","solutions L"];)
neuper@37991	1067	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	1068	(*val p = e_pos';
neuper@37906	1069	val c = [];
neuper@37906	1070	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1071	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1072	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	1073
neuper@37906	1074	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1075	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1076	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1077	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1078	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1079	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1080	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59267	1081	case f of FormKF "[x = 2, x = -2]" => ()
neuper@38031	1082	\| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
neuper@37906	1083
neuper@37906	1084	"----------------- polyeq.sml end ------------------";
neuper@37906	1085
neuper@37906	1086	(Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:)
neuper@37906	1087	(WN.19.3.03 ---v-)
neuper@37906	1088	(3(b))val (bdv,v) = (str2term "bdv", str2term "R1");
neuper@37906	1089	val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
neuper@37926	1090	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1091	term2str t';
neuper@37906	1092	"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
neuper@37906	1093	(WN.19.3.03 ---^-)
neuper@37906	1094
neuper@37906	1095	(3(c))val (bdv,v) = (str2term "bdv", str2term "p");
neuper@37906	1096	val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
neuper@37926	1097	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1098	term2str t';
neuper@37906	1099	"y ^^^ 2 + -2 * x * p = 0";
neuper@37906	1100
neuper@37906	1101	(3(d))val (bdv,v) = (str2term "bdv", str2term "x2");
neuper@37906	1102	val t = str2term
neuper@37906	1103	"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	1104	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1105	term2str t';
neuper@37906	1106	"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	1107	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
neuper@37906	1108	term2str t';
neuper@37906	1109	"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	1110
neuper@37906	1111	(3(e))val (bdv,v) = (str2term "bdv", str2term "a");
neuper@37906	1112	val t = str2term
neuper@37906	1113	"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
neuper@37926	1114	val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1115	(die _unsichtbare_ Klammern sind genau wie gew"unscht)
neuper@37906	1116
neuper@37906	1117
neuper@37906	1118	val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
neuper@37906	1119	trace_rewrite:=true;
neuper@37906	1120	rewrite_set_ thy false expand_binoms t;
neuper@37906	1121	trace_rewrite:=false;
neuper@37906	1122
neuper@37906	1123
neuper@37906	1124	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	1125	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	1126	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
s1210629013@55445	1127	reset_states ();
neuper@37906	1128	CalcTree
neuper@42319	1129	[(["equality ((3::real)x - 1 - (5x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
neuper@37991	1130	("PolyEq",["univariate","equation"],["no_met"]))];
neuper@37906	1131	Iterator 1;
neuper@37906	1132	moveActiveRoot 1;
wneuper@59248	1133	autoCalculate 1 CompleteCalc;
neuper@37906	1134	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@42394	1135	interSteps 1 ([1],Res)
neuper@42394	1136	(BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?);
neuper@37906	1137
neuper@42394	1138	"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394	1139	"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394	1140	"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
neuper@42394	1141	val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
neuper@42394	1142	val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
neuper@42394	1143	val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
neuper@42394	1144	(* steps in rls d2_polyeq_bdv_only_simplify:*)
neuper@42248	1145
neuper@42394	1146	(-6 x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(bdv,x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
neuper@42394	1147	t \|> term2str; t \|> atomty;
neuper@42394	1148	val thm = num_str @{thm d2_prescind1};
wneuper@59188	1149	thm \|> Thm.prop_of \|> term2str; thm \|> Thm.prop_of \|> atomty;
neuper@42394	1150	val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
neuper@42394	1151
neuper@42394	1152	(x (-6 + 5 * x) = 0 : Rewrite_Inst (["(bdv,x)"],("d2_reduce_equation1",""))
neuper@42394	1153	--> x = 0 \| -6 + 5 * x = 0*)
neuper@42394	1154	t' \|> term2str; t' \|> atomty;
neuper@42394	1155	val thm = num_str @{thm d2_reduce_equation1};
wneuper@59188	1156	thm \|> Thm.prop_of \|> term2str; thm \|> Thm.prop_of \|> atomty;
neuper@42394	1157	val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t'';
neuper@42394	1158	(* NONE with d2_reduce_equation1: "(bdv(a +bbdv)=0) = ((bdv=0)\|(a+b*bdv=0))"
neuper@42394	1159	instead d2_reduce_equation1: "(bdv(a +bbdv)=0) = ((bdv=0)\|(a+b*bdv=(0::real)))"
neuper@42394	1160	*)
neuper@42394	1161	if term2str t'' = "x = 0 \| -6 + 5 * x = 0" then ()
neuper@42394	1162	else error "rls d2_polyeq_bdv_only_simplify broken";
neuper@42394	1163
neuper@42394	1164

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59267	aab874fdd910
child 59367	fb6f5ef2c647
permissions	-rw-r--r--