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 "-----------------------------------------------------------------";
12 "----------- tests on predicates in problems ---------------------";
13 "----------- test matching problems --------------------------0---";
14 "----------- lin.eq degree_0 -------------------------------------";
15 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
16 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
17 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
18 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
19 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
20 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
21 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
22 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
23 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
24 "-----------------------------------------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
28 val c = []; print_depth 5;
30 "----------- tests on predicates in problems ---------------------";
31 "----------- tests on predicates in problems ---------------------";
32 "----------- tests on predicates in problems ---------------------";
37 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
38 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
39 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
40 else error "polyeq.sml: diff.behav. in lhs";
42 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
43 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
44 if (term2str t) = "True" then ()
45 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
47 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
48 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
49 if (term2str t) = "False" then ()
50 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
52 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
53 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
54 if (term2str t) = "True" then ()
55 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
57 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
58 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
59 if (term2str t) = "True" then ()
60 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
63 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
64 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
65 if (term2str t) = "True" then ()
66 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
68 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
69 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
70 if (term2str t) = "True" then ()
71 else error "polyeq.sml: diff.behav. in has_degree_in_in";
73 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
74 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
75 if (term2str t) = "False" then ()
76 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
78 val t4 = (term_of o the o (parse thy))
79 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
80 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
81 if (term2str t) = "False" then ()
82 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
84 val t5 = (term_of o the o (parse thy))
85 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
86 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
87 if (term2str t) = "True" then ()
88 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
90 "----------- test matching problems --------------------------0---";
91 "----------- test matching problems --------------------------0---";
92 "----------- test matching problems --------------------------0---";
93 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
94 if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
95 Matches' {Find = [Correct "solutions L"],
97 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
98 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
99 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
101 then () else error "match_pbl [expanded,univariate,equation]";
103 if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
104 Matches' {Find = [Correct "solutions L"],
106 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
107 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
108 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
109 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
111 "----------- lin.eq degree_0 -------------------------------------";
112 "----------- lin.eq degree_0 -------------------------------------";
113 "----------- lin.eq degree_0 -------------------------------------";
114 "----- d0_false ------";
115 (*=== inhibit exn WN110906 ======================================================
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 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
120 val (p,_,f,nxt,_,pt) = me nxt p c pt;
121 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
122 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
123 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
125 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
126 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
127 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
129 "----- d0_true ------";
131 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
132 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
133 ["PolyEq","solve_d0_polyeq_equation"]);
134 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
135 val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
141 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
142 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
143 ============ inhibit exn WN110906 ============================================*)
145 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
146 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
147 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
148 "----- d2_pqformula1 ------!!!!";
149 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
151 ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
152 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
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;
163 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
164 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
165 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
166 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
167 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
168 val (mI,m) = mk_tac'_ tac;
169 val Appl m = applicable_in p pt m;
170 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
171 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
173 term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
174 terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
175 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
176 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
177 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
178 "\"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\","^
179 "\"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\"]";
180 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
181 member op = specsteps mI (*false*);
182 (*loc_solve_ (mI,m) ptp;
183 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
184 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
186 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
187 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
188 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
189 val thy' = get_obj g_domID pt (par_pblobj pt p);
190 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
192 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
193 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
194 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
195 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
196 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
197 val thy = assoc_thy thy';
198 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
199 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
200 ... Assoc ... is correct*)
201 "~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
202 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
203 1 < length l (*true*);
204 val up = drop_last l;
207 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
208 ... ???? ... is correct*)
209 "~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
210 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
211 val l = drop_last l; (*comes from e, goes to Abs*)
212 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
213 val i = mk_Free (i, T);
214 val E = upd_env E (i, v);
215 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
216 val [(tac_, mout, ptree, pos', xxx)] = ss;
217 val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
218 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
219 ... Assoc ... is correct*)
220 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
221 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
222 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
223 val ctxt = get_ctxt pt (p,p_)
224 val p' = lev_on p : pos;
225 (* WAS val NotAss = assod pt d m stac
226 ... Ass ... is correct*)
227 "~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
228 (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
231 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
232 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
234 "----- d2_pqformula1_neg ------";
236 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
237 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
238 (*val p = e_pos'; val c = [];
239 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
240 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
241 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
242 val (p,_,f,nxt,_,pt) = me nxt p c pt;
243 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
244 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 ([1],Res) False Or_to_List)*)
249 val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 ([2],Res) [] Check_elementwise "Assumptions"*)
252 val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt;
254 val asm = get_assumptions_ pt p;
255 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
256 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
258 "----- d2_pqformula2 ------";
259 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
260 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
261 ["PolyEq","solve_d2_polyeq_pq_equation"]);
262 (*val p = e_pos'; val c = [];
263 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
264 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
265 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
266 val (p,_,f,nxt,_,pt) = me nxt p c pt;
267 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
268 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
269 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
271 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
272 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
273 val (p,_,f,nxt,_,pt) = me nxt p c pt;
274 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
275 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
278 "----- d2_pqformula2_neg ------";
279 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
280 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
281 ["PolyEq","solve_d2_polyeq_pq_equation"]);
282 (*val p = e_pos'; val c = [];
283 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
284 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
285 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
286 val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
290 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
291 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
292 val (p,_,f,nxt,_,pt) = me nxt p c pt;
293 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
294 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
295 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
298 "----- d2_pqformula3 ------";
300 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
301 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
302 ["PolyEq","solve_d2_polyeq_pq_equation"]);
303 (*val p = e_pos'; val c = [];
304 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
305 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
306 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
307 val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
309 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
310 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
311 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
312 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
313 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
314 val (p,_,f,nxt,_,pt) = me nxt p c pt;
315 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
316 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
318 "----- d2_pqformula3_neg ------";
319 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
320 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
321 ["PolyEq","solve_d2_polyeq_pq_equation"]);
322 (*val p = e_pos'; val c = [];
323 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
324 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
325 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
326 val (p,_,f,nxt,_,pt) = me nxt p c pt;
327 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
328 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
329 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
330 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
332 val (p,_,f,nxt,_,pt) = me nxt p c pt;
333 "TODO 2 + x + x^^^2 = 0";
334 "TODO 2 + x + x^^^2 = 0";
335 "TODO 2 + x + x^^^2 = 0";
338 "----- d2_pqformula4 ------";
339 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
340 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
341 ["PolyEq","solve_d2_polyeq_pq_equation"]);
342 (*val p = e_pos'; val c = [];
343 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
344 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
345 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
346 val (p,_,f,nxt,_,pt) = me nxt p c pt;
347 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
348 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
349 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
350 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
351 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
352 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
353 val (p,_,f,nxt,_,pt) = me nxt p c pt;
354 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
355 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
357 "----- d2_pqformula4_neg ------";
358 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
359 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
360 ["PolyEq","solve_d2_polyeq_pq_equation"]);
361 (*val p = e_pos'; val c = [];
362 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
363 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
364 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
365 val (p,_,f,nxt,_,pt) = me nxt p c pt;
366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
370 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 "TODO 2 + x + 1*x^^^2 = 0";
372 "TODO 2 + x + 1*x^^^2 = 0";
373 "TODO 2 + x + 1*x^^^2 = 0";
375 "----- d2_pqformula5 ------";
376 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
377 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
378 ["PolyEq","solve_d2_polyeq_pq_equation"]);
379 (*val p = e_pos'; val c = [];
380 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
381 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
382 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
383 val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
385 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
390 val (p,_,f,nxt,_,pt) = me nxt p c pt;
391 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
392 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
394 "----- d2_pqformula6 ------";
395 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
396 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
397 ["PolyEq","solve_d2_polyeq_pq_equation"]);
398 (*val p = e_pos'; val c = [];
399 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
400 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
401 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
403 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
404 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
405 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
406 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 val (p,_,f,nxt,_,pt) = me nxt p c pt;
410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
411 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
413 "----- d2_pqformula7 ------";
415 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
416 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
417 ["PolyEq","solve_d2_polyeq_pq_equation"]);
418 (*val p = e_pos'; val c = [];
419 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
420 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
421 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
422 val (p,_,f,nxt,_,pt) = me nxt p c pt;
423 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
424 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
425 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
426 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
427 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
428 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
429 val (p,_,f,nxt,_,pt) = me nxt p c pt;
430 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
431 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
433 "----- d2_pqformula8 ------";
434 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
435 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
436 ["PolyEq","solve_d2_polyeq_pq_equation"]);
437 (*val p = e_pos'; val c = [];
438 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
439 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
441 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
442 val (p,_,f,nxt,_,pt) = me nxt p c pt;
443 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
444 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
445 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
446 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
448 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
449 val (p,_,f,nxt,_,pt) = me nxt p c pt;
450 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
451 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
453 "----- d2_pqformula9 ------";
454 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
455 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
456 ["PolyEq","solve_d2_polyeq_pq_equation"]);
457 (*val p = e_pos'; val c = [];
458 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
461 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
466 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
468 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
470 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
473 "----- d2_pqformula10_neg ------";
474 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
475 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
476 ["PolyEq","solve_d2_polyeq_pq_equation"]);
477 (*val p = e_pos'; val c = [];
478 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
479 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
481 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
482 val (p,_,f,nxt,_,pt) = me nxt p c pt;
483 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
484 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
485 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
486 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
487 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
488 val (p,_,f,nxt,_,pt) = me nxt p c pt;
489 "TODO 4 + x^^^2 = 0";
490 "TODO 4 + x^^^2 = 0";
491 "TODO 4 + x^^^2 = 0";
493 "----- d2_pqformula10 ------";
494 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
495 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
496 ["PolyEq","solve_d2_polyeq_pq_equation"]);
497 (*val p = e_pos'; val c = [];
498 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
499 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
501 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
502 val (p,_,f,nxt,_,pt) = me nxt p c pt;
503 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
504 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
505 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
506 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
507 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
508 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
509 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
510 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
512 "----- d2_pqformula9_neg ------";
513 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
514 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
515 ["PolyEq","solve_d2_polyeq_pq_equation"]);
516 (*val p = e_pos'; val c = [];
517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
520 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
522 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
524 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;
527 "TODO 4 + 1*x^^^2 = 0";
528 "TODO 4 + 1*x^^^2 = 0";
529 "TODO 4 + 1*x^^^2 = 0";
531 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
532 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
533 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
535 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
536 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
537 ["PolyEq","solve_d2_polyeq_abc_equation"]);
538 (*val p = e_pos'; val c = [];
539 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
540 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
542 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
543 val (p,_,f,nxt,_,pt) = me nxt p c pt;
544 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
547 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
548 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
549 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
550 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
551 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
553 val fmz = ["equality ( 1 +(-1)*x + 2*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 = e_pos'; val c = [];
557 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
558 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
560 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
561 val (p,_,f,nxt,_,pt) = me nxt p c pt;
562 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
563 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
564 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
565 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
566 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
567 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
568 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
569 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
572 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
573 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
574 ["PolyEq","solve_d2_polyeq_abc_equation"]);
575 (*val p = e_pos'; val c = [];
576 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
577 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
579 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
580 val (p,_,f,nxt,_,pt) = me nxt p c pt;
581 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
582 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
583 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
584 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
585 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
587 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
588 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
590 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
591 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
592 ["PolyEq","solve_d2_polyeq_abc_equation"]);
593 (*val p = e_pos'; val c = [];
594 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
595 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
597 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
598 val (p,_,f,nxt,_,pt) = me nxt p c pt;
599 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
600 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
601 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
602 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
603 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
604 val (p,_,f,nxt,_,pt) = me nxt p c pt;
605 "TODO 1 + x + 2*x^^^2 = 0";
606 "TODO 1 + x + 2*x^^^2 = 0";
607 "TODO 1 + x + 2*x^^^2 = 0";
609 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
610 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
611 ["PolyEq","solve_d2_polyeq_abc_equation"]);
612 (*val p = e_pos'; val c = [];
613 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
614 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
616 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
617 val (p,_,f,nxt,_,pt) = me nxt p c pt;
618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
621 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
622 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
623 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
624 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
625 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
627 val fmz = ["equality ( 2 + 1*x + 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 = e_pos'; val c = [];
631 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
632 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
634 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
635 val (p,_,f,nxt,_,pt) = me nxt p c pt;
636 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
637 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
638 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
639 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
640 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
641 val (p,_,f,nxt,_,pt) = me nxt p c pt;
642 "TODO 2 + 1*x + x^^^2 = 0";
643 "TODO 2 + 1*x + x^^^2 = 0";
644 "TODO 2 + 1*x + x^^^2 = 0";
647 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
648 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
649 ["PolyEq","solve_d2_polyeq_abc_equation"]);
650 (*val p = e_pos'; val c = [];
651 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
652 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
654 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
655 val (p,_,f,nxt,_,pt) = me nxt p c pt;
656 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
657 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
658 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
659 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
660 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
661 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
662 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
663 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
665 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
666 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
667 ["PolyEq","solve_d2_polyeq_abc_equation"]);
668 (*val p = e_pos'; val c = [];
669 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
670 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
672 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
673 val (p,_,f,nxt,_,pt) = me nxt p c pt;
674 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
675 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
676 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
677 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
678 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
679 val (p,_,f,nxt,_,pt) = me nxt p c pt;
680 "TODO 2 + x + x^^^2 = 0";
681 "TODO 2 + x + x^^^2 = 0";
682 "TODO 2 + x + x^^^2 = 0";
685 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
686 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
687 ["PolyEq","solve_d2_polyeq_abc_equation"]);
688 (*val p = e_pos'; val c = [];
689 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
690 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
692 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
693 val (p,_,f,nxt,_,pt) = me nxt p c pt;
694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
695 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
696 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
697 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
698 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
699 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
700 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
701 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
703 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
704 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
705 ["PolyEq","solve_d2_polyeq_abc_equation"]);
706 (*val p = e_pos'; val c = [];
707 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
708 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
710 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
711 val (p,_,f,nxt,_,pt) = me nxt p c pt;
712 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
713 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
714 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
715 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
716 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
717 "TODO 8+ 2*x^^^2 = 0";
718 "TODO 8+ 2*x^^^2 = 0";
719 "TODO 8+ 2*x^^^2 = 0";
722 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
723 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
724 (*val p = e_pos'; val c = [];
725 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
726 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
728 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
729 val (p,_,f,nxt,_,pt) = me nxt p c pt;
730 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
731 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
732 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
733 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
734 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
735 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
736 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
737 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
740 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
741 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
742 (*val p = e_pos'; val c = [];
743 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
744 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
746 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
747 val (p,_,f,nxt,_,pt) = me nxt p c pt;
748 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
749 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
750 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
751 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
752 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
758 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
759 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
760 ["PolyEq","solve_d2_polyeq_abc_equation"]);
761 (*val p = e_pos'; val c = [];
762 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
763 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
765 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
766 val (p,_,f,nxt,_,pt) = me nxt p c pt;
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
770 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
771 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
772 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
773 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
774 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
776 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
777 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
778 ["PolyEq","solve_d2_polyeq_abc_equation"]);
779 (*val p = e_pos'; val c = [];
780 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
781 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
783 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
784 val (p,_,f,nxt,_,pt) = me nxt p c pt;
785 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
786 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
787 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
788 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
789 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
790 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
791 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
792 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
795 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
796 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
797 ["PolyEq","solve_d2_polyeq_abc_equation"]);
798 (*val p = e_pos'; val c = [];
799 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
800 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
802 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
803 val (p,_,f,nxt,_,pt) = me nxt p c pt;
804 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
805 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
806 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
807 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
808 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
809 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
810 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
811 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
814 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
815 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
816 ["PolyEq","solve_d2_polyeq_abc_equation"]);
817 (*val p = e_pos'; val c = [];
818 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
819 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
821 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
822 val (p,_,f,nxt,_,pt) = me nxt p c pt;
823 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
824 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
825 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
826 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
827 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
828 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
829 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
830 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
832 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
833 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
834 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
835 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
836 "solveFor x","solutions L"];
838 ("PolyEq",["degree_2","expanded","univariate","equation"],
839 ["PolyEq","complete_square"]);
840 (* val p = e_pos'; val c = [];
841 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
842 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
844 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
845 val (p,_,f,nxt,_,pt) = me nxt p c pt;
846 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
847 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
848 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
849 (*Apply_Method ("PolyEq","complete_square")*)
850 val (p,_,f,nxt,_,pt) = me nxt p c pt;
851 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
852 val (p,_,f,nxt,_,pt) = me nxt p c pt;
853 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
854 val (p,_,f,nxt,_,pt) = me nxt p c pt;
855 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
856 val (p,_,f,nxt,_,pt) = me nxt p c pt;
857 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
858 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
859 val (p,_,f,nxt,_,pt) = me nxt p c pt;
860 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
861 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
862 val (p,_,f,nxt,_,pt) = me nxt p c pt;
863 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
864 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
865 val (p,_,f,nxt,_,pt) = me nxt p c pt;
866 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
867 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
868 val (p,_,f,nxt,_,pt) = me nxt p c pt;
869 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
870 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
871 val (p,_,f,nxt,_,pt) = me nxt p c pt;
872 (*"x = -2 | x = 4" nxt = Or_to_List*)
873 val (p,_,f,nxt,_,pt) = me nxt p c pt;
874 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
875 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
877 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
878 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
880 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
881 else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
884 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
885 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
886 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
887 "---- test the erls ----";
888 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
889 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
891 (*if t'= "HOL.True" then ()
892 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
894 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
895 "solveFor x","solutions L"];
897 ("PolyEq",["degree_2","expanded","univariate","equation"],
898 ["PolyEq","complete_square"]);
899 (* val p = e_pos'; val c = [];
900 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
901 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
903 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
904 val (p,_,f,nxt,_,pt) = me nxt p c pt;
905 val (p,_,f,nxt,_,pt) = me nxt p c pt;
906 val (p,_,f,nxt,_,pt) = me nxt p c pt;
907 val (p,_,f,nxt,_,pt) = me nxt p c pt;
908 val (p,_,f,nxt,_,pt) = me nxt p c pt;
909 val (p,_,f,nxt,_,pt) = me nxt p c pt;
910 val (p,_,f,nxt,_,pt) = me nxt p c pt;
911 (*Apply_Method ("PolyEq","complete_square")*)
912 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
914 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
915 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
916 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
917 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
918 "solveFor x","solutions L"];
920 ("PolyEq",["degree_2","expanded","univariate","equation"],
921 ["PolyEq","complete_square"]);
922 (* val p = e_pos'; val c = [];
923 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
924 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
926 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
927 val (p,_,f,nxt,_,pt) = me nxt p c pt;
928 val (p,_,f,nxt,_,pt) = me nxt p c pt;
929 val (p,_,f,nxt,_,pt) = me nxt p c pt;
930 val (p,_,f,nxt,_,pt) = me nxt p c pt;
931 val (p,_,f,nxt,_,pt) = me nxt p c pt;
932 val (p,_,f,nxt,_,pt) = me nxt p c pt;
933 val (p,_,f,nxt,_,pt) = me nxt p c pt;
934 (*Apply_Method ("PolyEq","complete_square")*)
935 val (p,_,f,nxt,_,pt) = me nxt p c pt;
936 val (p,_,f,nxt,_,pt) = me nxt p c pt;
937 val (p,_,f,nxt,_,pt) = me nxt p c pt;
938 val (p,_,f,nxt,_,pt) = me nxt p c pt;
939 val (p,_,f,nxt,_,pt) = me nxt p c pt;
940 val (p,_,f,nxt,_,pt) = me nxt p c pt;
941 val (p,_,f,nxt,_,pt) = me nxt p c pt;
942 val (p,_,f,nxt,_,pt) = me nxt p c pt;
943 val (p,_,f,nxt,_,pt) = me nxt p c pt;
944 val (p,_,f,nxt,_,pt) = me nxt p c pt;
946 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
947 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
950 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
951 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
952 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
953 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
954 "solveFor x","solutions L"];
956 ("PolyEq",["degree_2","expanded","univariate","equation"],
957 ["PolyEq","complete_square"]);
958 (* val p = e_pos'; val c = [];
959 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
960 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
962 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
963 val (p,_,f,nxt,_,pt) = me nxt p c pt;
964 val (p,_,f,nxt,_,pt) = me nxt p c pt;
965 val (p,_,f,nxt,_,pt) = me nxt p c pt;
966 val (p,_,f,nxt,_,pt) = me nxt p c pt;
967 val (p,_,f,nxt,_,pt) = me nxt p c pt;
968 val (p,_,f,nxt,_,pt) = me nxt p c pt;
969 val (p,_,f,nxt,_,pt) = me nxt p c pt;
970 val (p,_,f,nxt,_,pt) = me nxt p c pt;
971 val (p,_,f,nxt,_,pt) = me nxt p c pt;
972 val (p,_,f,nxt,_,pt) = me nxt p c pt;
974 val (p,_,f,nxt,_,pt) = me nxt p c pt;
975 val (p,_,f,nxt,_,pt) = me nxt p c pt;
976 val (p,_,f,nxt,_,pt) = me nxt p c pt;
977 val (p,_,f,nxt,_,pt) = me nxt p c pt;
978 val (p,_,f,nxt,_,pt) = me nxt p c pt;
979 val (p,_,f,nxt,_,pt) = me nxt p c pt;
980 val (p,_,f,nxt,_,pt) = me nxt p c pt;
981 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
982 (*WN.2.5.03 TODO FIXME Matthias ?
986 (~1,EdUndef,0,Nundef,
987 "[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)]"))
989 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
990 this will be simplified [x = a, x = b] to by Factor.ML*)
993 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
994 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
995 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
996 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
997 "solveFor x","solutions L"];
999 ("PolyEq",["degree_2","expanded","univariate","equation"],
1000 ["PolyEq","complete_square"]);
1001 (* val p = e_pos'; val c = [];
1002 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1003 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1005 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1006 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1007 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1008 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1009 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1010 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1011 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1012 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1013 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1014 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1015 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1016 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1017 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1018 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1019 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1020 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1021 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1024 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1025 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1026 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1027 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1028 "solveFor x","solutions L"];
1030 ("PolyEq",["degree_2","expanded","univariate","equation"],
1031 ["PolyEq","complete_square"]);
1032 (* val p = e_pos'; val c = [];
1033 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1034 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1036 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1037 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1038 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1039 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1040 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1041 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1042 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1043 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1044 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1045 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1046 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1047 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1049 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1050 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1053 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1054 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1055 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1056 (*EP-17 Schalk_I_p86_n5*)
1057 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1058 (* refine fmz ["univariate","equation"];
1060 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1063 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1064 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1066 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1067 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1070 Model_Problem ["normalize","polynomial","univariate","equation"])
1072 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1073 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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;
1079 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1081 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1084 Model_Problem ["degree_1","polynomial","univariate","equation"])
1086 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1089 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1090 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1091 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1092 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1093 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1094 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1095 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1098 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1099 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1100 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1101 (*is in rlang.sml, too*)
1102 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1103 "solveFor x","solutions L"];
1104 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1106 (*val p = e_pos'; val c = [];
1107 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1108 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1110 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1111 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1115 Model_Problem ["normalize","polynomial","univariate","equation"])
1117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1125 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1130 Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
1132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1139 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1140 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1146 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1147 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1148 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1149 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1152 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1153 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1154 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1163 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1164 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1166 "----------------- polyeq.sml end ------------------";
1168 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1169 (*WN.19.3.03 ---v-*)
1170 (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1171 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1172 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1174 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1175 (*WN.19.3.03 ---^-*)
1177 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1178 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1179 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1181 "y ^^^ 2 + -2 * x * p = 0";
1183 (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1185 "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";
1186 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1188 "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";
1189 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1191 "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";
1193 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1195 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1196 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1197 (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1200 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1201 trace_rewrite:=true;
1202 rewrite_set_ thy false expand_binoms t;
1203 trace_rewrite:=false;
1206 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1207 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1208 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1211 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1212 ("PolyEq",["univariate","equation"],["no_met"]))];
1215 autoCalculate 1 CompleteCalc;
1216 val ((pt,p),_) = get_calc 1; show_pt pt;
1218 interSteps 1 ([1],Res) (*no Rewrite_Set...*);
1220 ============ inhibit exn WN110906 ==============================================*)