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