1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Sep 18 12:15:59 2019 +0200
1.3 @@ -0,0 +1,892 @@
1.4 +(* Title: Knowledge/polyeq-1.sml
1.5 + testexamples for PolyEq, poynomial equations and equational systems
1.6 + Author: Richard Lang 2003
1.7 + (c) due to copyright terms
1.8 +WN030609: some expls dont work due to unfinished handling of 'expanded terms';
1.9 + others marked with TODO have to be checked, too.
1.10 +*)
1.11 +
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"------ polyeq-1.sml ---------------------------------------------";
1.16 +"----------- tests on predicates in problems ---------------------";
1.17 +"----------- test matching problems ------------------------------";
1.18 +"----------- lin.eq degree_0 -------------------------------------";
1.19 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.20 +"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.21 +"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.22 +"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.23 +"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.24 +"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.25 +"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.26 +"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.27 +"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.28 +"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.29 +"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.30 +"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.31 +"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.32 +"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.33 +"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.34 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.35 +"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.36 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.37 +"-----------------------------------------------------------------";
1.38 +"------ polyeq-2.sml ---------------------------------------------";
1.39 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.40 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.41 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.42 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.43 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.44 +"----------- rls make_polynomial_in ------------------------------";
1.45 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.46 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.47 +"-----------------------------------------------------------------";
1.48 +"-----------------------------------------------------------------";
1.49 +
1.50 +"----------- tests on predicates in problems ---------------------";
1.51 +"----------- tests on predicates in problems ---------------------";
1.52 +"----------- tests on predicates in problems ---------------------";
1.53 +(* trace_rewrite:=true;
1.54 + trace_rewrite:=false;
1.55 +*)
1.56 + val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.57 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.58 + if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.59 + else error "polyeq.sml: diff.behav. in lhs";
1.60 +
1.61 + val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.62 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.63 + if (term2str t) = "True" then ()
1.64 + else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.65 +
1.66 + val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.67 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.68 + if (term2str t) = "False" then ()
1.69 + else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.70 +
1.71 + val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.72 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.73 + if (term2str t) = "True" then ()
1.74 + else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.75 +
1.76 + val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.77 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.78 + if (term2str t) = "True" then ()
1.79 + else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.80 +
1.81 +
1.82 + val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.83 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.84 + if (term2str t) = "True" then ()
1.85 + else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.86 +
1.87 + val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.88 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.89 + if (term2str t) = "True" then ()
1.90 + else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.91 +
1.92 + val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.93 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.94 + if (term2str t) = "False" then ()
1.95 + else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.96 +
1.97 + val t4 = (Thm.term_of o the o (parse thy))
1.98 + "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.99 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.100 + if (term2str t) = "False" then ()
1.101 + else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.102 +
1.103 + val t5 = (Thm.term_of o the o (parse thy))
1.104 + "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.105 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.106 + if (term2str t) = "True" then ()
1.107 + else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.108 +
1.109 +"----------- test matching problems --------------------------0---";
1.110 +"----------- test matching problems --------------------------0---";
1.111 +"----------- test matching problems --------------------------0---";
1.112 +val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.113 +if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
1.114 + Matches' {Find = [Correct "solutions L"],
1.115 + With = [],
1.116 + Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.117 + Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
1.118 + Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
1.119 + Relate = []}
1.120 +then () else error "match_pbl [expanded,univariate,equation]";
1.121 +
1.122 +if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
1.123 + Matches' {Find = [Correct "solutions L"],
1.124 + With = [],
1.125 + Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.126 + Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
1.127 + Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
1.128 +then () else error "match_pbl [degree_2,expanded,univariate,equation]";
1.129 +
1.130 +"----------- lin.eq degree_0 -------------------------------------";
1.131 +"----------- lin.eq degree_0 -------------------------------------";
1.132 +"----------- lin.eq degree_0 -------------------------------------";
1.133 +"----- d0_false ------";
1.134 +val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
1.135 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.136 + ["PolyEq","solve_d0_polyeq_equation"]);
1.137 +(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
1.138 +TODO: change to "equality (x + -1*x = (0::real))"
1.139 + and search for an appropriate problem and method.
1.140 +
1.141 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.142 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.143 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.144 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.145 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.146 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.147 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.148 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.149 + | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.150 +
1.151 +"----- d0_true ------";
1.152 +val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
1.153 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.154 + ["PolyEq","solve_d0_polyeq_equation"]);
1.155 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.156 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.157 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.158 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.159 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.160 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.161 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.162 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
1.163 + | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
1.164 +============ inhibit exn WN110914 ============================================*)
1.165 +
1.166 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.167 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.168 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.169 +"----- d2_pqformula1 ------!!!!";
1.170 +val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
1.171 +val (dI',pI',mI') =
1.172 + ("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
1.173 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.174 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.175 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.176 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.177 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.178 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.179 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.180 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
1.181 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.182 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.183 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.184 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.185 +
1.186 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.187 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.188 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
1.189 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.190 +val (mI,m) = mk_tac'_ tac;
1.191 +val Appl m = applicable_in p pt m;
1.192 +val Check_elementwise' (trm1, str, (trm2, trms)) = m;
1.193 +term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.194 +str = "Assumptions";
1.195 +term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.196 +terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.197 + " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
1.198 + "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
1.199 + "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
1.200 + "\"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\","^
1.201 + "\"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\"]";
1.202 +(*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
1.203 +member op = specsteps mI (*false*);
1.204 +(*loc_solve_ (mI,m) ptp;
1.205 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
1.206 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
1.207 +(*solve m (pt, pos);
1.208 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
1.209 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.210 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.211 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.212 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.213 + val d = e_rls;
1.214 +(*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.215 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
1.216 +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
1.217 + (scr as Prog (h $ body),d), (Pstate (E,l,a,v,S,b), ctxt)) =
1.218 + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
1.219 +val thy = assoc_thy thy';
1.220 +l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
1.221 +(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
1.222 + ... Assoc ... is correct*)
1.223 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
1.224 + ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.225 +1 < length l (*true*);
1.226 +val up = drop_last l;
1.227 + term2str (go up sc);
1.228 + (go up sc);
1.229 +(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
1.230 + ... ???? ... is correct*)
1.231 +"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
1.232 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
1.233 + val l = drop_last l; (*comes from e, goes to Abs*)
1.234 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.235 + val i = mk_Free (i, T);
1.236 + val E = upd_env E (i, v);
1.237 +(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
1.238 +val [(tac_, mout, ctree, pos', xxx)] = ss;
1.239 +val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
1.240 +(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
1.241 + ... Assoc ... is correct*)
1.242 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
1.243 + ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
1.244 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
1.245 + val ctxt = get_ctxt pt (p,p_)
1.246 + val p' = lev_on p : pos;
1.247 +(* WAS val NotAss = associate pt d (m, stac)
1.248 + ... Ass ... is correct*)
1.249 +"~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
1.250 + (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
1.251 +term2str consts;
1.252 +term2str consts';
1.253 +if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
1.254 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.255 +
1.256 +"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.257 +"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.258 +"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.259 +"----- d2_pqformula1_neg ------";
1.260 +val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
1.261 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.262 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.263 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.264 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.265 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.266 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.267 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.268 +(*### or2list False
1.269 + ([1],Res) False Or_to_List)*)
1.270 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.271 +(*### or2list False
1.272 + ([2],Res) [] Check_elementwise "Assumptions"*)
1.273 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.274 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.275 +val asm = get_assumptions_ pt p;
1.276 +if f2str f = "[]" andalso
1.277 + terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.278 + "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
1.279 +else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.280 +
1.281 +"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.282 +"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.283 +"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.284 +"----- d2_pqformula2 ------";
1.285 +val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.286 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.287 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.288 +(*val p = e_pos';
1.289 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.290 +val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
1.291 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.292 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.293 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.294 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.295 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.296 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.297 +
1.298 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.299 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.300 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.301 +case f of FormKF "[x = 2, x = -1]" => ()
1.302 + | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.303 +
1.304 +
1.305 +"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.306 +"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.307 +"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.308 +"----- d2_pqformula3 ------";
1.309 +(*EP-9*)
1.310 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.311 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.312 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.313 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.314 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.315 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.316 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.317 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.318 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.319 +
1.320 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.321 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.322 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.323 +case f of FormKF "[x = 1, x = -2]" => ()
1.324 + | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.325 +
1.326 +
1.327 +"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.328 +"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.329 +"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.330 +"----- d2_pqformula3_neg ------";
1.331 +val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.332 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.333 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.334 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.335 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.336 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.337 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.338 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.339 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.340 +
1.341 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.342 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.343 +"TODO 2 + x + x^^^2 = 0";
1.344 +"TODO 2 + x + x^^^2 = 0";
1.345 +"TODO 2 + x + x^^^2 = 0";
1.346 +
1.347 +"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.348 +"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.349 +"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.350 +"----- d2_pqformula4 ------";
1.351 +val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.352 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.353 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.354 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.355 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.356 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.357 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.358 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.359 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.360 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.361 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.362 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.363 +case f of FormKF "[x = 1, x = -2]" => ()
1.364 + | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
1.365 +
1.366 +"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.367 +"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.368 +"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.369 +"----- d2_pqformula5 ------";
1.370 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.371 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.372 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.373 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.374 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.375 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.376 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.377 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.378 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.379 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.380 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.381 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.382 +case f of FormKF "[x = 0, x = -1]" => ()
1.383 + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.384 +
1.385 +"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.386 +"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.387 +"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.388 +"----- d2_pqformula6 ------";
1.389 +val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.390 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.391 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.392 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.393 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.394 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.395 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.396 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.397 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.398 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.399 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.400 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.401 +case f of FormKF "[x = 0, x = -1]" => ()
1.402 + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.403 +
1.404 +"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.405 +"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.406 +"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.407 +"----- d2_pqformula7 ------";
1.408 +(*EP-10*)
1.409 +val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
1.410 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.411 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.412 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.413 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.414 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.415 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.416 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.417 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.418 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.419 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.420 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.421 +case f of FormKF "[x = 0, x = -1]" => ()
1.422 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.423 +
1.424 +"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.425 +"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.426 +"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.427 +"----- d2_pqformula8 ------";
1.428 +val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.429 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.430 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.431 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.432 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.433 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.434 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.435 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.436 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.437 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.438 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.439 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.440 +case f of FormKF "[x = 0, x = -1]" => ()
1.441 + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.442 +
1.443 +"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.444 +"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.445 +"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.446 +"----- d2_pqformula9 ------";
1.447 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.448 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.449 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.450 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.451 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.452 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.453 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.454 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.455 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.456 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.457 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.458 +case f of FormKF "[x = 2, x = -2]" => ()
1.459 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.460 +
1.461 +
1.462 +"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.463 +"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.464 +"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.465 +"----- d2_pqformula9_neg ------";
1.466 +val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.467 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.468 + ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.469 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.470 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.471 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.472 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.473 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.474 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.475 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.476 +"TODO 4 + 1*x^^^2 = 0";
1.477 +"TODO 4 + 1*x^^^2 = 0";
1.478 +"TODO 4 + 1*x^^^2 = 0";
1.479 +
1.480 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.481 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.482 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.483 +val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.484 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.485 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.486 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.487 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.488 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.489 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.490 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.491 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.492 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.493 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.494 +case f of FormKF "[x = 1, x = -1 / 2]" => ()
1.495 + | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.496 +
1.497 +"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.498 +"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.499 +"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.500 +val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.501 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.502 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.503 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.504 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.505 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.506 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.507 +
1.508 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.509 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.510 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.511 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.512 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.513 +"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.514 +
1.515 +
1.516 +"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.517 +"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.518 +"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.519 +(*EP-11*)
1.520 +val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.521 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.522 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.523 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.524 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.525 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.526 +
1.527 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.528 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.529 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.530 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.531 +
1.532 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.533 +case f of FormKF "[x = 1 / 2, x = -1]" => ()
1.534 + | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.535 +
1.536 +
1.537 +"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.538 +"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.539 +"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.540 +val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.541 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.542 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.543 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.544 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.545 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.546 +
1.547 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.548 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.549 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.550 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.551 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.552 +"TODO 1 + x + 2*x^^^2 = 0";
1.553 +"TODO 1 + x + 2*x^^^2 = 0";
1.554 +"TODO 1 + x + 2*x^^^2 = 0";
1.555 +
1.556 +
1.557 +val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.558 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.559 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.560 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.561 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.562 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.563 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.564 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.565 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.566 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.567 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.568 +case f of FormKF "[x = 1, x = -2]" => ()
1.569 + | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.570 +
1.571 +val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.572 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.573 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.574 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.575 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.576 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.577 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.578 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.579 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.580 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.581 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.582 +"TODO 2 + 1*x + x^^^2 = 0";
1.583 +"TODO 2 + 1*x + x^^^2 = 0";
1.584 +"TODO 2 + 1*x + x^^^2 = 0";
1.585 +
1.586 +(*EP-12*)
1.587 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.588 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.589 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.590 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.591 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.592 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.593 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.594 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.595 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.596 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.597 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.598 +case f of FormKF "[x = 1, x = -2]" => ()
1.599 + | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.600 +
1.601 +val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.602 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.603 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.604 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.605 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.606 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.607 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.608 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.609 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.610 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.611 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.612 +"TODO 2 + x + x^^^2 = 0";
1.613 +"TODO 2 + x + x^^^2 = 0";
1.614 +"TODO 2 + x + x^^^2 = 0";
1.615 +
1.616 +(*EP-13*)
1.617 +val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.618 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.619 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.620 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.621 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.622 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.623 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.624 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.625 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.626 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.627 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.628 +case f of FormKF "[x = 2, x = -2]" => ()
1.629 + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.630 +
1.631 +val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.632 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.633 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.634 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.635 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.636 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.637 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.638 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.639 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.640 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.641 +"TODO 8+ 2*x^^^2 = 0";
1.642 +"TODO 8+ 2*x^^^2 = 0";
1.643 +"TODO 8+ 2*x^^^2 = 0";
1.644 +
1.645 +(*EP-14*)
1.646 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.647 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.648 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.649 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.650 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.651 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.652 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.653 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.654 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.655 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.656 +case f of FormKF "[x = 2, x = -2]" => ()
1.657 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.658 +
1.659 +
1.660 +val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
1.661 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.662 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.663 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.664 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.665 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.666 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.667 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.668 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.669 +"TODO 4+ x^^^2 = 0";
1.670 +"TODO 4+ x^^^2 = 0";
1.671 +"TODO 4+ x^^^2 = 0";
1.672 +
1.673 +(*EP-15*)
1.674 +val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.675 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.676 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.677 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.678 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.679 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.680 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.681 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.682 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.683 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.684 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.685 +case f of FormKF "[x = 0, x = -1]" => ()
1.686 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.687 +
1.688 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.689 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.690 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.691 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.692 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.693 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.694 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.695 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.696 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.697 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.698 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.699 +case f of FormKF "[x = 0, x = -1]" => ()
1.700 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.701 +
1.702 +(*EP-16*)
1.703 +val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.704 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.705 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.706 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.707 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.708 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.709 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.710 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.711 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.712 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.713 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.714 +case f of FormKF "[x = 0, x = -1 / 2]" => ()
1.715 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.716 +
1.717 +(*EP-//*)
1.718 +val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
1.719 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.720 + ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.721 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.722 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.723 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.724 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.725 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.726 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.727 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.728 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.729 +case f of FormKF "[x = 0, x = -1]" => ()
1.730 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.731 +
1.732 +
1.733 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.734 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.735 +"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.736 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.737 +see --- val rls = calculate_RootRat > calculate_Rational ---
1.738 +calculate_RootRat was a TODO with 2002, requires re-design.
1.739 +see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
1.740 +*)
1.741 + val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.742 + "solveFor x","solutions L"];
1.743 + val (dI',pI',mI') =
1.744 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.745 + ["PolyEq","complete_square"]);
1.746 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.747 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.748 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.749 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.750 +
1.751 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.752 +(*Apply_Method ("PolyEq","complete_square")*)
1.753 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.754 +(*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.755 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.756 +(*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
1.757 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.758 +(*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
1.759 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.760 +(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.761 + 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.762 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.763 +(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.764 + -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.765 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.766 +(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.767 + -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
1.768 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.769 +(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.770 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
1.771 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.772 +(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
1.773 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
1.774 + NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
1.775 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.776 +(*"x = -2 | x = 4" nxt = Or_to_List*)
1.777 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.778 +(*"[x = -2, x = 4]" nxt = Check_Postcond*)
1.779 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.780 +(* FIXXXME
1.781 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
1.782 + | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.783 +*)
1.784 +if f2str f =
1.785 +"[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
1.786 +(*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
1.787 +then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.788 +
1.789 +
1.790 +"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.791 +"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.792 +"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.793 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.794 +see --- val rls = calculate_RootRat > calculate_Rational ---*)
1.795 +val thy = @{theory PolyEq};
1.796 +val ctxt = Proof_Context.init_global thy;
1.797 +val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1.798 +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
1.799 +
1.800 +val rls = complete_square;
1.801 +val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.802 +term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.803 +
1.804 +val thm = num_str @{thm square_explicit1};
1.805 +val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
1.806 +term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.807 +
1.808 +val thm = num_str @{thm root_plus_minus};
1.809 +val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.810 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.811 + "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.812 +
1.813 +(*the thm bdv_explicit2* here required to be constrained to ::real*)
1.814 +val thm = num_str @{thm bdv_explicit2};
1.815 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
1.816 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.817 + "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.818 +
1.819 +val thm = num_str @{thm bdv_explicit3};
1.820 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
1.821 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.822 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.823 +
1.824 +val thm = num_str @{thm bdv_explicit2};
1.825 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
1.826 +term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.827 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.828 +
1.829 +val rls = calculate_RootRat;
1.830 +val SOME (t,asm) = rewrite_set_ thy true rls t;
1.831 +if term2str t =
1.832 + "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
1.833 +(*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
1.834 +then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.835 +(*SHOULD BE: term2str = "x = -2 | x = 4;*)
1.836 +
1.837 +
1.838 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.839 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.840 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.841 +"---- test the erls ----";
1.842 + val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.843 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.844 + val t' = term2str t;
1.845 + (*if t'= "HOL.True" then ()
1.846 + else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.847 +(* *)
1.848 + val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.849 + "solveFor x","solutions L"];
1.850 + val (dI',pI',mI') =
1.851 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.852 + ["PolyEq","complete_square"]);
1.853 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.854 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.855 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.856 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.857 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.858 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.859 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.860 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.861 + (*Apply_Method ("PolyEq","complete_square")*)
1.862 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.863 +
1.864 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.865 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.866 +"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.867 + val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1.868 + "solveFor x","solutions L"];
1.869 + val (dI',pI',mI') =
1.870 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.871 + ["PolyEq","complete_square"]);
1.872 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.873 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.874 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.875 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.876 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.877 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.878 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.879 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.880 + (*Apply_Method ("PolyEq","complete_square")*)
1.881 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.882 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.883 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.884 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.885 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.886 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.887 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.888 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.889 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.890 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.891 +(* FIXXXXME n1.,
1.892 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1.893 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1.894 +*)
1.895 +