2 imports "Isac.Build_Isac"
5 ML \<open>open ML_System\<close>
9 open Test_Code; CalcTreeTEST;
10 open LItool; arguments_from_model;
18 open Error_Pattern_Def;
20 open Ctree; append_problem;
26 open Auto_Prog; rule2stac;
33 open Solve; (* NONE *)
34 open ContextC; transfer_asms_from_to;
35 open Tactic; (* NONE *)
38 open P_Model; (* NONE *)
43 open Rule_Set; Sequence;
51 (*ML_file "BridgeJEdit/parseC.sml"*)
53 section \<open>code for copy & paste ===============================================================\<close>
55 "~~~~~ fun xxx , args:"; val () = ();
56 "~~~~~ and xxx , args:"; val () = ();
57 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
58 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
60 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
61 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
63 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
64 (*/------------------- step into XXXXX -----------------------------------------------------\*)
65 (*-------------------- stop step into XXXXX -------------------------------------------------*)
66 (*\------------------- step into XXXXX -----------------------------------------------------/*)
67 (*-------------------- contiue step into XXXXX ----------------------------------------------*)
68 (*/------------------- check entry to XXXXX ------------------------------------------------\*)
69 (*\------------------- check entry to XXXXX ------------------------------------------------/*)
70 (*/------------------- check within XXXXX --------------------------------------------------\*)
71 (*\------------------- check within XXXXX --------------------------------------------------/*)
72 (*/------------------- check result of XXXXX -----------------------------------------------\*)
73 (*\------------------- check result of XXXXX -----------------------------------------------/*)
75 (*/------------------- build new fun XXXXX -------------------------------------------------\*)
76 (*\------------------- build new fun XXXXX -------------------------------------------------/*)
84 declare [[show_types]]
85 declare [[show_sorts]]
86 find_theorems "?a <= ?a"
92 ML_command \<open>Pretty.writeln prt\<close>
93 declare [[ML_print_depth = 999]]
94 declare [[ML_exception_trace]]
97 section \<open>===================================================================================\<close>
104 section \<open>===================================================================================\<close>
111 section \<open>======== check Knowledge/polyeq-1.sml =============================================\<close>
114 (* Title: Knowledge/polyeq-1.sml
115 testexamples for PolyEq, poynomial equations and equational systems
116 Author: Richard Lang 2003
117 (c) due to copyright terms
118 WN030609: some expls dont work due to unfinished handling of 'expanded terms';
119 others marked with TODO have to be checked, too.
122 "-----------------------------------------------------------------";
123 "table of contents -----------------------------------------------";
124 "-----------------------------------------------------------------";
125 "------ polyeq- 1.sml ---------------------------------------------";
126 "----------- tests on predicates in problems ---------------------";
127 "----------- test matching problems ------------------------------";
128 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
129 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
130 "----------- lin.eq degree_0 -------------------------------------";
131 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
132 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
133 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
134 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
135 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
136 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
137 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
138 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
139 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
140 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
141 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
142 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
143 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
144 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
145 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
146 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
147 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
148 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
149 "-----------------------------------------------------------------";
150 "------ polyeq- 2.sml ---------------------------------------------";
151 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
152 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
153 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
154 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
155 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
156 "----------- rls make_polynomial_in ------------------------------";
157 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
158 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
159 "-----------------------------------------------------------------";
160 "-----------------------------------------------------------------";
163 "----------- tests on predicates in problems ---------------------";
164 "----------- tests on predicates in problems ---------------------";
165 "----------- tests on predicates in problems ---------------------";
166 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
167 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
168 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
169 else error "polyeq.sml: diff.behav. in lhs";
171 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
172 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
173 if (UnparseC.term t) = "True" then ()
174 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
176 val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
177 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
178 if (UnparseC.term t) = "False" then ()
179 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
181 val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
182 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
183 if (UnparseC.term t) = "True" then ()
184 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
186 val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
187 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
188 if (UnparseC.term t) = "True" then ()
189 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
191 val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
192 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
193 if (UnparseC.term t) = "True" then ()
194 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
196 val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
197 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
198 if (UnparseC.term t) = "True" then ()
199 else error "polyeq.sml: diff.behav. in has_degree_in_in";
202 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
203 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
205 UnparseC.term t = "- 1 = 2";
206 \<close> text \<open> (*"((sqrt(x)) has_degree_in x) = 2" --- = "- 1 = 2" START HERE*)
207 if (UnparseC.term t) = "False" then ()
208 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
211 val t4 = (Thm.term_of o the o (TermC.parse thy))
212 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
213 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
214 if (UnparseC.term t) = "False" then ()
215 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
217 val t5 = (Thm.term_of o the o (TermC.parse thy))
218 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
219 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
220 if (UnparseC.term t) = "True" then ()
221 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
223 \<close> text \<open> (* M_Match.match_pbl [expanded,univariate,equation] *)
224 "----------- test matching problems --------------------------0---";
225 "----------- test matching problems --------------------------0---";
226 "----------- test matching problems --------------------------0---";
227 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
228 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
229 M_Match.Matches' {Find = [Correct "solutions L"],
231 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
232 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
233 Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
235 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
237 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
238 M_Match.Matches' {Find = [Correct "solutions L"],
240 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
241 Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
242 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
243 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
246 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
247 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
248 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
249 (*##################################################################################
250 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
252 (*Aufgabe zum Einstieg in die Arbeit...*)
253 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
254 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
255 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
257 "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
259 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
261 "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
262 (* bei Verwendung von "size_of-term" nach MG :*)
263 (*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
265 (*wir holen 'a' wieder aus der Klammerung heraus...*)
266 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
268 "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
269 (* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
272 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
274 "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
275 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
276 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
278 (*das rewriting l"asst sich beobachten mit
279 Rewrite.trace_on := false; (*true false*)
282 "------ 15.11.02 --------------------------";
283 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
284 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
285 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
287 Rewrite.trace_on := false; (*true false*)
288 (* Anwenden einer Regelmenge aus Termorder.ML: *)
290 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
293 rewrite_set_ thy false discard_parentheses t;
297 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
299 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
302 rewrite_set_ thy false discard_parentheses t;
304 "1 + (x + b * x) * a + a \<up> 2";
306 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
308 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
311 rewrite_set_ thy false discard_parentheses t;
313 "1 + b * a + (7 + x) * a \<up> 2";
316 Prog_Expr.thy grundlegende Algebra
320 RootRat.thy Wurzen + Br"uche
321 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
323 get_thm Termorder.thy "bdv_n_collect";
324 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
326 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
328 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
331 rewrite_set_ thy false discard_parentheses t;
333 "(7 + x) * a \<up> 2";
335 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
337 val t = (Thm.term_of o the o (parseold thy)) "7";
338 ##################################################################################*)
342 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
343 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
344 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
345 val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
346 val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
347 val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
349 val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
350 val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
351 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
352 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
354 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
355 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
357 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
358 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
360 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
361 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
363 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
364 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
365 ord_make_polynomial_in true thy substx (aa, bb);
368 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
369 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
370 ord_make_polynomial_in true thy substa (aa, bb);
371 false; (* => GREATER *)
373 (* und nach dem Re-engineering der Termorders in den 'rulesets'
374 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
375 val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
376 val x = (Thm.term_of o the o (TermC.parse thy)) "x";
377 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
378 val b = (Thm.term_of o the o (TermC.parse thy)) "b";
379 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
380 if UnparseC.term t' = "b + x + a" then ()
381 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
383 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
385 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
386 if UnparseC.term t' = "a + b + x" then ()
387 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
389 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
390 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
391 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
393 UnparseC.term t' = "- 6 + - (5 * x) + x \<up> 3 + - (x \<up> 2) + - (x \<up> 3) +\n- (14 * x \<up> 2)"
394 \<close> text \<open> (* TODO.ThmC.numerals_to_Free termorder.sml diff.behav ord_make_polynomial_in*)
395 if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
396 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
398 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
399 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
400 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
402 val ttt' = "(3*x + 5)/18";
403 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
404 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
405 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
406 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
408 (*============ inhibit exn WN120316 ==============================================
409 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
410 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
411 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
412 ============ inhibit exn WN120316 ==============================================*)
416 "----------- lin.eq degree_0 -------------------------------------";
417 "----------- lin.eq degree_0 -------------------------------------";
418 "----------- lin.eq degree_0 -------------------------------------";
419 "----- d0_false ------";
420 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
421 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
422 ["PolyEq", "solve_d0_polyeq_equation"]);
423 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
424 TODO: change to "equality (x + - 1*x = (0::real))"
425 and search for an appropriate problem and method.
427 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
428 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
431 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
432 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
433 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
434 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
435 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
437 "----- d0_true ------";
438 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
439 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
440 ["PolyEq", "solve_d0_polyeq_equation"]);
441 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
442 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
443 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
444 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
445 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
446 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
447 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
448 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
449 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
450 ============ inhibit exn WN110914 ============================================*)
452 \<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 4 = - 1 / 4" z =
453 - 1 * (- 1 / 4 / 2) + sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2 \<or>
455 - 1 * (- 1 / 4 / 2) + - 1 * (sqrt ((- 1 / 4) \<up> 2 + - 4 * (- 1 / 8)) / 2) = NONE*)
456 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
457 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
458 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
459 "----- d2_pqformula1 ------!!!!";
460 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
462 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
463 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
464 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
466 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
471 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
472 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
473 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
474 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
476 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
477 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
478 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
479 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
481 if p = ([], Res) andalso
482 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
483 case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
484 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
487 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
488 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
489 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
490 "----- d2_pqformula1_neg ------";
491 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
492 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
493 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
494 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
500 ([1],Res) False Or_to_List)*)
501 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
503 ([2],Res) [] Check_elementwise "Assumptions"*)
504 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
505 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
506 val asm = Ctree.get_assumptions pt p;
507 if f2str f = "[]" andalso
508 UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
509 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
510 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
512 \<close> text \<open> (*TOODOO rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 1 * (- 1 / 2) + sqrt ((- 1) \<up> 2 + 8) / 2 \<or>
513 x = - 1 * (- 1 / 2) + - 1 * (sqrt ((- 1) \<up> 2 + 8) / 2) = NONE*)
514 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
515 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
516 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
517 "----- d2_pqformula2 ------";
518 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
519 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
520 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
521 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
522 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
523 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
531 case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
532 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
535 \<close> text \<open> (*see TOODOO.1*)
536 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
537 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
538 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
539 "----- d2_pqformula3 ------";
541 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
542 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
543 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
544 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
545 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
551 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
552 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
554 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
555 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
559 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
560 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
561 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
562 "----- d2_pqformula3_neg ------";
563 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
564 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
565 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
566 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
567 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
568 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
571 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;
575 "TODO 2 + x + x \<up> 2 = 0";
576 "TODO 2 + x + x \<up> 2 = 0";
577 "TODO 2 + x + x \<up> 2 = 0";
579 \<close> text \<open> (*see TOODOO.1*)
580 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
581 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
582 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
583 "----- d2_pqformula4 ------";
584 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
585 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
586 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
587 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
588 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
595 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
596 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
598 \<close> text \<open> (* loops*)
599 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
600 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
601 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
602 "----- d2_pqformula5 ------";
603 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
604 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
605 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
606 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
607 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
608 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
609 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
610 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
611 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
612 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
613 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
614 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
615 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
616 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
618 \<close> text \<open> (* loops*)
619 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
620 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
621 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
622 "----- d2_pqformula6 ------";
623 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
624 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
625 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
626 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
627 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
628 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
629 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
630 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
631 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
635 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
636 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
638 \<close> text \<open> (* loops*)
639 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
640 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
641 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
642 "----- d2_pqformula7 ------";
644 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
645 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
646 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
647 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
648 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
653 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
654 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
655 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
656 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
657 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
659 \<close> text \<open> (* loops*)
660 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
661 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
662 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
663 "----- d2_pqformula8 ------";
664 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
665 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
666 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
667 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
668 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
669 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
670 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
671 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
672 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
673 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
674 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
675 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
676 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
677 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
679 \<close> text \<open> (*see TOODOO.1*)
680 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
681 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
682 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
683 "----- d2_pqformula9 ------";
684 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
685 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
686 ["PolyEq", "solve_d2_polyeq_pq_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 Test_Out.FormKF "[x = 2, x = - 2]" => ()
696 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
700 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
701 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
702 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
703 "----- d2_pqformula9_neg ------";
704 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
705 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
706 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
707 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
708 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
711 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
712 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
713 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
714 "TODO 4 + 1*x \<up> 2 = 0";
715 "TODO 4 + 1*x \<up> 2 = 0";
716 "TODO 4 + 1*x \<up> 2 = 0";
718 \<close> text \<open> (*see TOODOO.1*)
719 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
720 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
721 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
722 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
723 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
724 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
725 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
726 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
727 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
728 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
729 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
730 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
731 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
732 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
733 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
734 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
737 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
738 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
739 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
740 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
741 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
742 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
743 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
744 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
748 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
749 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
750 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
751 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
752 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
753 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
756 \<close> text \<open> (*see TOODOO.1*)
757 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
758 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
759 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
761 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
762 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
763 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
764 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
765 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
766 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
769 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
770 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
771 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
774 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
775 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
779 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
780 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
781 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
782 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
783 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
784 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
785 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
786 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
787 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
789 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
790 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
791 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
792 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
793 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
794 "TODO 1 + x + 2*x \<up> 2 = 0";
795 "TODO 1 + x + 2*x \<up> 2 = 0";
796 "TODO 1 + x + 2*x \<up> 2 = 0";
799 \<close> text \<open> (*f = Test_Out.FormKF "[]" *)
800 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
801 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
802 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
803 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
804 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
805 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
806 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
807 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
808 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
809 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
810 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
811 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
812 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
815 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
816 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
817 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
818 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
819 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
820 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
821 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
822 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
823 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
824 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
825 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
826 "TODO 2 + 1*x + x \<up> 2 = 0";
827 "TODO 2 + 1*x + x \<up> 2 = 0";
828 "TODO 2 + 1*x + x \<up> 2 = 0";
830 \<close> text \<open> (*f = Test_Out.FormKF "[]" *)
832 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
833 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
834 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
835 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
836 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
837 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
838 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
839 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
840 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
841 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
842 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
843 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
844 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
847 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
848 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
849 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
850 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
851 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
853 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
855 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
857 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
858 "TODO 2 + x + x \<up> 2 = 0";
859 "TODO 2 + x + x \<up> 2 = 0";
860 "TODO 2 + x + x \<up> 2 = 0";
862 \<close> text \<open> (*f = Test_Out.FormKF "[]" *)
864 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
865 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
866 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
867 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
868 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
869 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
870 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
871 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
874 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
875 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
876 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
879 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
880 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
881 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
882 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
883 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
884 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
885 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
886 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
887 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
888 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
889 "TODO 8+ 2*x \<up> 2 = 0";
890 "TODO 8+ 2*x \<up> 2 = 0";
891 "TODO 8+ 2*x \<up> 2 = 0";
893 \<close> text \<open> (*f = Test_Out.FormKF "[]" *)
895 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
896 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
897 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
898 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
899 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
900 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
901 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
902 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
903 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
904 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
905 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
906 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
910 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
911 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
912 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
913 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
914 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
915 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
916 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
917 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
918 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
919 "TODO 4+ x \<up> 2 = 0";
920 "TODO 4+ x \<up> 2 = 0";
921 "TODO 4+ x \<up> 2 = 0";
923 \<close> text \<open> (*f = Test_Out.FormKF "[]"*)
925 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
926 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
927 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
928 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
929 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
930 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
931 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
932 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
933 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
934 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
935 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
936 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
937 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
939 \<close> text \<open> (* loops*)
940 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
941 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
942 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
943 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
944 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
945 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
946 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
947 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
948 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
949 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
950 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
951 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
952 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
954 \<close> text \<open> (* loops*)
956 val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
957 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
958 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
959 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
960 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
961 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
962 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
963 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
964 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
965 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
968 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
970 \<close> text \<open> (* loops*)
972 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
973 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
974 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
975 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
976 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
977 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
978 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
979 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
980 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
981 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
982 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
983 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
984 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
987 \<close> text \<open> (* loops*)
988 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
989 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
990 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
991 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
992 see --- val rls = calculate_RootRat > calculate_Rational ---
993 calculate_RootRat was a TODO with 2002, requires re-design.
994 see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
996 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
997 "solveFor x", "solutions L"];
999 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1000 ["PolyEq", "complete_square"]);
1001 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1002 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1003 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1004 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1006 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1007 (*Apply_Method ("PolyEq", "complete_square")*)
1008 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1009 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1010 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1011 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
1012 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1013 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
1014 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1015 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1016 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1017 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1018 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1019 - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1020 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1021 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1022 - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
1023 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1024 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1025 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
1026 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1027 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
1028 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
1029 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
1030 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1031 (*"x = - 2 | x = 4" nxt = Or_to_List*)
1032 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1033 (*"[x = - 2, x = 4]" nxt = Check_Postcond*)
1034 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1036 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
1037 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1040 "[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))]"
1041 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1042 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1045 \<close> text \<open> (* loops*)
1046 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1047 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1048 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1049 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1050 see --- val rls = calculate_RootRat > calculate_Rational ---*)
1051 val thy = @ {theory PolyEq};
1052 val ctxt = Proof_Context.init_global thy;
1053 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1054 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1056 val rls = complete_square;
1057 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1058 UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
1060 val thm = ThmC.numerals_to_Free @{thm square_explicit1};
1061 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1062 UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
1064 val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1065 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1066 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1067 "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1069 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1070 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1071 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1072 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1073 "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1075 val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1076 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1077 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1078 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1080 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1081 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1082 UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1083 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1085 val rls = calculate_RootRat;
1086 val SOME (t,asm) = rewrite_set_ thy true rls t;
1087 if UnparseC.term t =
1088 "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"
1089 (*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
1090 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1091 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
1095 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1096 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1097 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1098 "---- test the erls ----";
1099 val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
1100 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1101 val t' = UnparseC.term t;
1102 (*if t'= "HOL.True" then ()
1103 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1105 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
1106 "solveFor x", "solutions L"];
1108 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1109 ["PolyEq", "complete_square"]);
1110 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1111 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1112 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1113 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1114 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1115 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1116 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1117 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1118 (*Apply_Method ("PolyEq", "complete_square")*)
1119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1121 \<close> text \<open> (* loops*)
1122 \<close> text \<open> (*f = Test_Out.FormKF "[]" *)
1123 \<close> text \<open> (*see TOODOO.1*)
1125 \<close> text \<open> (* loops*)
1126 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1127 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1128 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1129 val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
1130 "solveFor x", "solutions L"];
1132 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1133 ["PolyEq", "complete_square"]);
1134 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1135 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1136 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1137 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1138 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1139 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1140 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1141 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1142 (*Apply_Method ("PolyEq", "complete_square")*)
1143 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1144 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1145 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1146 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1147 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1148 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1149 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1150 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1151 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1152 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1154 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1155 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1159 \<close> text \<open> (*-------^^^^^ polyeq-1.sml------------vvv diff.sml-------TOODOO----------------*)
1162 section \<open>======== check Knowledge/diff.sml =================================================\<close>
1165 (* Title: test/Tools/isac/Knowledge/diff.sml
1166 Author: Walther Neuper
1167 Use is subject to license terms.
1169 "-----------------------------------------------------------------------------------------------";
1170 "-----------------------------------------------------------------------------------------------";
1171 "table of contents -----------------------------------------------------------------------------";
1172 "-----------------------------------------------------------------------------------------------";
1173 "----------- problemtype --------------------------------";
1174 "----------- for correction of diff_const ---------------";
1175 "----------- for correction of diff_quot ----------------";
1176 "----------- differentiate by rewrite -------------------";
1177 "----------- differentiate: me (*+ tacs input*) ---------";
1178 "----------- 1.5.02 me from script ----------------------";
1179 "----------- primed id ----------------------------------";
1180 "----------- diff_conv, sym_diff_conv -------------------";
1181 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
1182 "----------- autoCalculate diff after_simplification ----";
1183 "----------- autoCalculate differentiate_equality -------";
1184 "----------- tests for examples -------------------------";
1185 "------------inform for x \<up> 2+x+1 -------------------------";
1186 "--------------------------------------------------------";
1187 "--------------------------------------------------------";
1188 "--------------------------------------------------------";
1191 val thy = @{theory "Diff"};
1193 "----------- problemtype --------------------------------";
1194 "----------- problemtype --------------------------------";
1195 "----------- problemtype --------------------------------";
1196 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
1198 Find =["derivative f_f'"],
1200 Relate=[]}:string ppc;
1201 val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt;
1203 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))",
1204 "differentiateFor x", "derivative f_f'"];
1205 val chkorg = map (the o (TermC.parse thy)) org;
1207 Problem.from_store ["derivative_of", "function"];
1208 MethodC.from_store ["diff", "differentiate_on_R"];
1210 "----------- for correction of diff_const ---------------";
1211 "----------- for correction of diff_const ---------------";
1212 "----------- for correction of diff_const ---------------";
1213 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
1214 val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
1215 case rewrite_set_ thy false erls_diff t of
1216 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
1217 | _ => error "rewrite_set_ Not (x =!= a) changed";
1219 val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const";
1220 case rewrite_set_ thy false erls_diff t of
1221 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
1222 | _ => error "rewrite_set_ 2 is_const changed";
1224 val thm = @{thm diff_const};
1225 val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";
1226 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
1227 val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
1229 "----------- for correction of diff_quot ----------------";
1230 "----------- for correction of diff_quot ----------------";
1231 "----------- for correction of diff_quot ----------------";
1232 val thy = @{theory "Diff"};
1233 val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)";
1234 rewrite_set_ thy false erls_diff ct;
1236 val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))";
1237 val thm = @{thm diff_quot};
1239 (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1241 "----------- differentiate by rewrite -------------------";
1242 "----------- differentiate by rewrite -------------------";
1243 "----------- differentiate by rewrite -------------------";
1244 val thy = @{theory "Diff"};
1245 val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \<up> 2 + 3 * x + 4)";
1247 val thm = @{thm "diff_sum"};
1248 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1250 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1252 val thm = @{thm "diff_prod_const"};
1253 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1255 val thm = @{thm "diff_pow"};
1256 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1258 val thm = @{thm "diff_const"};
1259 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1261 val thm = @{thm "diff_var"};
1262 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1263 if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
1264 else error "diff.sml diff.behav. in rewrite 1";
1267 val rls = Test_simplify;
1268 val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \<up> (2 - 1) + 3 * 1 + 0";
1269 val (ct, _) = the (rewrite_set_ thy true rls ct);
1270 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
1272 "----------- differentiate: me (*+ tacs input*) ---------";
1273 "----------- differentiate: me (*+ tacs input*) ---------";
1274 "----------- differentiate: me (*+ tacs input*) ---------";
1275 val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)",
1276 "differentiateFor x", "derivative f_f'"];
1278 ("Diff",["derivative_of", "function"],
1279 ["diff", "diff_simpl"]);
1280 val p = e_pos'; val c = [];
1282 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1283 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1285 (*val nxt = ("Add_Given",
1286 Add_Given "functionTerm (d_d x (x \<up> #2 + #3 * x + #4))");*)
1287 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1289 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
1290 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1292 (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
1293 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1295 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
1296 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1298 (*val nxt = ("Specify_Problem",Specify_Problem pI');*)
1299 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1301 (*val nxt = ("Specify_Method",Specify_Method mI');*)
1302 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1304 (*val nxt = ("Apply_Method",Apply_Method mI');*)
1305 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1307 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
1308 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1310 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
1311 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1312 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
1313 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1315 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
1316 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1317 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1319 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow", "")));*)
1320 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1321 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1323 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
1324 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1325 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1327 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var", "")));*)
1328 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1329 if f2str f = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
1330 else error "diff.sml: diff.behav. in d_d x \<up> 2 + 3 * x + 4";
1332 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
1333 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1335 (*val nxt = ("Check_Postcond",Check_Postcond ("Diff", "differentiate_on_R"));*)
1336 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1338 (*val nxt = ("End_Proof'",End_Proof');*)
1339 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1340 if f2str f = "3 + 2 * x"
1341 then case nxt of End_Proof' => ()
1342 | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
1343 else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
1344 (*if f = EmptyMout then () else error "new behaviour in + tacs input"*)
1346 "----------- 1.5.02 me from script ----------------------";
1347 "----------- 1.5.02 me from script ----------------------";
1348 "----------- 1.5.02 me from script ----------------------";
1349 (*exp_Diff_No- 1.xml*)
1350 val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)",
1351 "differentiateFor x", "derivative f_f'"];
1353 ("Diff",["derivative_of", "function"],
1354 ["diff", "diff_simpl"]);
1355 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1356 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1357 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1358 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1359 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1360 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1361 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1363 (*nxt = ("Apply_Method",Apply_Method ("Diff", "differentiate_on_R*)
1364 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1366 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1367 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1368 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1369 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1370 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1371 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1372 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1373 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1374 case nxt of End_Proof' => ()
1375 | _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
1377 "----------- primed id ----------------------------------";
1378 "----------- primed id ----------------------------------";
1379 "----------- primed id ----------------------------------";
1380 val f_ = TermC.str2term "f_f::bool";
1381 val f = TermC.str2term "A = s * (a - s)";
1382 val v_ = TermC.str2term "v_v";
1383 val v = TermC.str2term "s";
1384 val screxp0 = TermC.str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
1385 TermC.atomty screxp0;
1387 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
1388 UnparseC.term screxp1;
1389 TermC.atomty screxp1;
1391 val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1;
1392 if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()
1393 else error "diff.sml: diff.behav. in 'primed'";
1396 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
1397 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
1398 \ in (((Try (Repeat (Rewrite frac_conv))) #> \
1399 \ (Try (Repeat (Rewrite root_conv))) #> \
1400 \ (Try (Repeat (Rewrite realpow_pow))) #> \
1402 \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \
1403 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
1404 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod )) Or \
1405 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot )) Or \
1406 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin )) Or \
1407 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain )) Or \
1408 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos )) Or \
1409 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain )) Or \
1410 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow )) Or \
1411 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain )) Or \
1412 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln )) Or \
1413 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain )) Or \
1414 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp )) Or \
1415 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain )) Or \
1416 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt )) Or \
1417 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
1418 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \
1419 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \
1420 \ (Repeat (Rewrite_Set make_polynomial)))) #> \
1421 \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
1422 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
1424 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
1427 \<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
1428 "----------- diff_conv, sym_diff_conv -------------------";
1429 "----------- diff_conv, sym_diff_conv -------------------";
1430 "----------- diff_conv, sym_diff_conv -------------------";
1431 val subs = [(TermC.str2term "bdv", TermC.str2term "x")];
1432 val rls = diff_conv;
1434 val t = TermC.str2term "2/x \<up> 2";
1435 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1436 if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
1438 val t = TermC.str2term "sqrt (x \<up> 3)";
1439 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1440 if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
1442 val t = TermC.str2term "2 / sqrt x \<up> 3";
1443 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1444 if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
1445 val rls = diff_sym_conv;
1447 val t = TermC.str2term "2 * x \<up> - 2";
1448 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1449 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
1451 val t = TermC.str2term "x \<up> (3 / 2)";
1452 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1453 if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
1455 val t = TermC.str2term "2 * x \<up> (-3 / 2)";
1456 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
1457 if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
1460 \<close> text \<open> (*loops autoCalculate (x \<up> 2 + x+ 1/x + 2/x \<up> 2)"*)
1461 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
1462 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
1463 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
1466 [(["functionTerm (x \<up> 2 + x+ 1/x + 2/x \<up> 2)",
1467 (*"functionTerm ((x \<up> 3) \<up> 5)",*)
1468 "differentiateFor x", "derivative f_f'"],
1469 ("Isac_Knowledge", ["derivative_of", "function"],
1470 ["diff", "differentiate_on_R"]))];
1473 autoCalculate 1 CompleteCalc;
1474 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1475 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
1476 "1 + 2 * x + - 1 / x \<up> 2 + -4 / x \<up> 3" then ()
1477 else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
1479 \<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
1480 "---------------------------------------------------------";
1483 [(["functionTerm (x \<up> 3 * x \<up> 5)",
1484 "differentiateFor x", "derivative f_f'"],
1485 ("Isac_Knowledge", ["derivative_of", "function"],
1486 ["diff", "differentiate_on_R"]))];
1489 autoCalculate 1 CompleteCalc;
1490 (* Rewrite.trace_on := false; (*true false*)
1491 LItool.trace_on := false;
1493 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1495 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
1496 "8 * x \<up> 7" then ()
1497 else error "diff.sml: differentiate_on_R (x \<up> 3 * x \<up> 5) changed";
1499 \<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
1500 "----------- autoCalculate diff after_simplification ----";
1501 "----------- autoCalculate diff after_simplification ----";
1502 "----------- autoCalculate diff after_simplification ----";
1505 [(["functionTerm (x \<up> 3 * x \<up> 5)",
1506 "differentiateFor x", "derivative f_f'"],
1507 ("Isac_Knowledge", ["derivative_of", "function"],
1508 ["diff", "after_simplification"]))];
1511 (* Rewrite.trace_on := true; (*true false*)
1512 LItool.trace_on := true;
1514 autoCalculate 1 CompleteCalc;
1515 (* Rewrite.trace_on := false; (*true false*)
1516 LItool.trace_on := false;
1518 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1519 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "8 * x \<up> 7"
1520 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1522 \<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
1523 "--------------------------------------------------------";
1526 [(["functionTerm ((x \<up> 3) \<up> 5)",
1527 "differentiateFor x", "derivative f_f'"],
1528 ("Isac_Knowledge", ["derivative_of", "function"],
1529 ["diff", "after_simplification"]))];
1532 autoCalculate 1 CompleteCalc;
1533 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1534 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
1535 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1537 \<close> text \<open> (*loops autoCalculate (A = s * (a - (s::real))*)
1538 "----------- autoCalculate differentiate_equality -------";
1539 "----------- autoCalculate differentiate_equality -------";
1540 "----------- autoCalculate differentiate_equality -------";
1543 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
1544 ("Isac_Knowledge", ["named", "derivative_of", "function"],
1545 ["diff", "differentiate_equality"]))];
1548 autoCalculate 1 CompleteCalc;
1549 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1552 "----------- tests for examples -------------------------";
1553 "----------- tests for examples -------------------------";
1554 "----------- tests for examples -------------------------";
1555 "----- TermC.parse errors";
1556 (*TermC.str2term "F = sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
1558 TermC.str2term "OO"; ---errors*)
1559 TermC.str2term "OOO";
1561 "----- thm 'diff_prod_const'";
1562 val subs = [(TermC.str2term "bdv", TermC.str2term "l")];
1563 val f = TermC.str2term "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
1565 \<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
1566 "------------inform for x \<up> 2+x+1 -------------------------";
1567 "------------inform for x \<up> 2+x+1 -------------------------";
1568 "------------inform for x \<up> 2+x+1 -------------------------";
1571 [(["functionTerm (x \<up> 2 + x + 1)",
1572 "differentiateFor x", "derivative f_f'"],
1573 ("Isac_Knowledge", ["derivative_of", "function"],
1574 ["diff", "differentiate_on_R"]))];
1577 autoCalculate 1 CompleteCalcHead;
1578 autoCalculate 1 (Steps 1);
1579 autoCalculate 1 (Steps 1);
1580 autoCalculate 1 (Steps 1);
1581 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1582 appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
1583 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1584 if existpt' ([3], Res) pt then ()
1585 else error "diff.sml: inform d_d x (x \<up> 2 + x + 1) doesnt work";
1588 \<close> text \<open> (*-------^^^^^ diff.sml------------vvv integrate.sml-----------TOODOO------------*)
1591 section \<open>======== check Knowledge/integrate.sml ============================================\<close>
1594 (* Title: test/Tools/isac/Knowledge/integrate.sml
1595 Author: Walther Neuper 050826
1596 (c) due to copyright terms
1598 "--------------------------------------------------------";
1599 "table of contents --------------------------------------";
1600 "--------------------------------------------------------";
1601 "----------- parsing ------------------------------------";
1602 "----------- integrate by rewriting ---------------------";
1603 "----------- test add_new_c, TermC.is_f_x ---------------------";
1604 "----------- simplify by ruleset reducing make_ratpoly_in";
1605 "----------- integrate by ruleset -----------------------";
1606 "----------- rewrite 3rd integration in 7.27 ------------";
1607 "----------- check probem type --------------------------";
1608 "----------- me method [diff,integration] ---------------";
1609 "----------- autoCalculate [diff,integration] -----------";
1610 "----------- me method [diff,integration,named] ---------";
1611 "----------- me met [diff,integration,named] Biegelinie.Q";
1612 "----------- method analog to rls 'integration' ---------";
1613 "--------------------------------------------------------";
1614 "--------------------------------------------------------";
1615 "--------------------------------------------------------";
1617 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
1618 they are used several times below; TODO remove duplicates*)
1619 val thy = @{theory "Integrate"};
1620 val ctxt = ThyC.to_ctxt thy;
1622 fun str2t str = parseNEW ctxt str |> the;
1623 fun term2s t = UnparseC.term_in_ctxt ctxt t;
1625 val conditions_in_integration_rules =
1626 Rule_Set.Repeat {id="conditions_in_integration_rules",
1628 rew_ord = ("termlessI",termlessI),
1629 erls = Rule_Set.Empty,
1630 srls = Rule_Set.Empty, calc = [], errpatts = [],
1631 rules = [(*for rewriting conditions in Thm's*)
1632 Eval ("Prog_Expr.occurs_in",
1633 eval_occurs_in "#occurs_in_"),
1634 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1635 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
1637 val subs = [(str2t "bdv::real", str2t "x::real")];
1639 fun rewrit thm str =
1640 fst (the (rewrite_inst_ thy tless_true
1641 conditions_in_integration_rules
1642 true subs thm str));
1646 "----------- parsing ------------------------------------";
1647 "----------- parsing ------------------------------------";
1648 "----------- parsing ------------------------------------";
1649 val t = TermC.str2term "Integral x D x";
1650 val t = TermC.str2term "Integral x \<up> 2 D x";
1652 Const (\<^const_name>\<open>Integral\<close>, _) $
1653 (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
1654 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
1656 val t = TermC.str2term "ff x is_f_x";
1657 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
1658 | _ => error "integrate.sml: parsing: ff x is_f_x";
1662 "----------- integrate by rewriting ---------------------";
1663 "----------- integrate by rewriting ---------------------";
1664 "----------- integrate by rewriting ---------------------";
1665 val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
1666 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
1668 val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x");
1669 if term2s str = "M' / EJ * x" then ()
1670 else error "Integral M'/EJ D x BY integral_const";
1672 val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
1673 if term2s str = "x \<up> 2 / 2" then ()
1674 else error "Integral x D x BY integral_var";
1676 val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
1677 if term2s str = "Integral x D x + Integral 1 D x" then ()
1678 else error "Integral x + 1 D x BY integral_add";
1680 val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
1681 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
1682 else error "Integral M'/EJ * x \<up> 3 D x BY integral_mult";
1684 val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
1685 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
1686 else error "integrate.sml Integral x \<up> 3 D x";
1690 "----------- test add_new_c, TermC.is_f_x ---------------------";
1691 "----------- test add_new_c, TermC.is_f_x ---------------------";
1692 "----------- test add_new_c, TermC.is_f_x ---------------------";
1693 val term = TermC.str2term "x \<up> 2 * c + c_2";
1694 val cc = new_c term;
1695 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
1697 val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy;
1698 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
1699 else error "intergrate.sml: diff. eval_add_new_c";
1701 val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_");
1702 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
1704 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
1705 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
1706 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
1708 val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
1709 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
1710 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
1711 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
1714 (*WN080222 replace call_new_c with add_new_c----------------------
1715 val term = str2t "new_c (c * x \<up> 2 + c_2)";
1716 val SOME (_,t') = eval_new_c 0 0 term 0;
1717 if term2s t' = "new_c c * x \<up> 2 + c_2 = c_3" then ()
1718 else error "integrate.sml: eval_new_c ???";
1720 val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2)";
1721 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
1722 if term2s t' = "matches (?u + new_c ?v) (x \<up> 2 / 2) = False" then ()
1723 else error "integrate.sml: matches new_c = False";
1725 val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2)";
1726 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
1727 if term2s t'="matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2) = True"
1728 then () else error "integrate.sml: matches new_c = True";
1730 val t = str2t "ff x TermC.is_f_x";
1731 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
1732 if term2s t' = "(ff x TermC.is_f_x) = True" then ()
1733 else error "integrate.sml: eval_is_f_x --> true";
1735 val t = str2t "q_0/2 * L * x TermC.is_f_x";
1736 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
1737 if term2s t' = "(q_0 / 2 * L * x TermC.is_f_x) = False" then ()
1738 else error "integrate.sml: eval_is_f_x --> false";
1740 val conditions_in_integration =
1741 Rule_Set.Repeat {id="conditions_in_integration",
1743 rew_ord = ("termlessI",termlessI),
1744 erls = Rule_Set.Empty,
1745 srls = Rule_Set.Empty, calc = [], errpatts = [],
1746 rules = [Eval ("Prog_Expr.matches",eval_matches ""),
1747 Eval ("Integrate.is_f_x",
1748 eval_is_f_x "is_f_x_"),
1749 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1750 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1754 fst (the (rewrite_inst_ thy tless_true
1755 conditions_in_integration true subs thm t));
1756 val t = rewrit call_for_new_c (str2t "x \<up> 2 / 2"); term2s t;
1757 val t = (rewrit call_for_new_c t)
1758 handle OPTION => str2t "no_rewrite";
1760 val t = rewrit call_for_new_c
1761 (str2t "ff x = q_0/2 *L*x"); term2s t;
1762 val t = (rewrit call_for_new_c
1763 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
1764 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
1765 --------------------------------------------------------------------*)
1769 "----------- simplify by ruleset reducing make_ratpoly_in";
1770 "----------- simplify by ruleset reducing make_ratpoly_in";
1771 "----------- simplify by ruleset reducing make_ratpoly_in";
1772 val thy = @{theory "Isac_Knowledge"};
1774 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
1776 "----- stepwise from the rulesets in simplify_Integral and below-----";
1777 val rls = norm_Rational_noadd_fractions;
1778 case rewrite_set_inst_ thy true subs rls t of
1779 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
1783 val rls = order_add_mult_in;
1784 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1785 assume flawed test setup hidden by "handle _ => ..."
1786 ERROR ord_make_polynomial_in called with subst = []
1787 val SOME (t,[]) = rewrite_set_ thy true rls t;
1788 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then()
1789 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
1790 \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
1793 val rls = discard_parentheses;
1794 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1795 assume flawed test setup hidden by "handle _ => ..."
1796 ERROR ord_make_polynomial_in called with subst = []
1797 val SOME (t,[]) = rewrite_set_ thy true rls t;
1798 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
1799 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
1800 \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
1803 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1805 (Rule_Set.append_rules "separate_bdv" collect_bdv
1806 [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1807 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1808 Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1809 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
1810 Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1811 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1812 Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})
1813 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1815 (*show_types := true; --- do we need type-constraint in thms? *)
1816 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
1817 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
1818 @{thm separate_1_bdv}; (*::?'a*)
1819 val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*)
1820 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
1821 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
1823 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
1824 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
1825 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
1828 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
1829 val rls = simplify_Integral;
1830 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1831 (* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
1832 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
1833 else error "integrate.sml, simplify_Integral #99";
1836 "........... 2nd integral ........................................";
1837 "........... 2nd integral ........................................";
1838 "........... 2nd integral ........................................";
1839 val thy = @{theory Biegelinie};
1840 val t = TermC.str2term
1841 "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
1843 val rls = simplify_Integral;
1844 (*TOODOO simplify_Integral broken (required for Biegelinie) ---------------------------------\\
1845 "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
1846 \<down> "Integral 1 / EI * ((L * q_0 / 4) * x \<up> 2 + (- 1 * q_0 / 6) * x \<up> 3) D x" broken
1848 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1849 if UnparseC.term t =
1850 "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
1851 then () else raise error "integrate.sml, simplify_Integral #198";
1853 val rls = integration_rules;
1854 val SOME (t,[]) = rewrite_set_ thy true rls t;
1856 if UnparseC.term t =
1857 "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
1858 then () else error "integrate.sml, simplify_Integral #199";
1859 -------------------------------------------------------------------------------------------//*)
1863 "----------- integrate by ruleset -----------------------";
1864 "----------- integrate by ruleset -----------------------";
1865 "----------- integrate by ruleset -----------------------";
1866 val thy = @{theory "Integrate"};
1867 val rls = integration_rules;
1868 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
1869 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1872 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
1873 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1874 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
1876 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
1877 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1878 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
1881 val rls = add_new_c;
1882 val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
1883 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1884 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
1885 else error "integrate.sml: diff.behav. in add_new_c simpl.";
1888 val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
1889 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1890 if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
1891 else error "integrate.sml: diff.behav. in add_new_c equation";
1894 val rls = simplify_Integral;
1895 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1896 val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
1897 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1898 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
1899 then () else error "integrate.sml: diff.behav. in simplify_I #1";
1902 val rls = integration;
1903 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1904 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
1905 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1906 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
1907 then () else error "integrate.sml: diff.behav. in integration #1";
1910 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
1911 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1912 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
1913 else error "integrate.sml: diff.behav. in integration #2";
1915 \<close> text \<open> (*TOODOO rls "integration" does NOT work anymore *)
1916 val t = (Thm.term_of o the o (TermC.parse thy))
1917 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
1918 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1919 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
1920 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
1921 then () else error "integrate.sml: diff.behav. in integration #3";
1923 \<close> text \<open> (*TOODOO rls "integration" does NOT work anymore *)
1924 val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
1925 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
1926 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
1927 then () else error "integrate.sml: diff.behav. in integration #4";
1930 "----------- rewrite 3rd integration in 7.27 ------------";
1931 "----------- rewrite 3rd integration in 7.27 ------------";
1932 "----------- rewrite 3rd integration in 7.27 ------------";
1933 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
1934 val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
1935 val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t;
1938 "Integral 1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2) D x";
1939 (*TOODOO simplify_Integral NOW weaker *)
1940 \<close> text \<open> (* TOODOO rls simplify_Integral <------------------------------ START HERE *)
1941 if UnparseC.term t =
1942 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
1943 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
1946 val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
1949 "c + Integral 1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2) D x";
1950 \<close> text \<open> (*TOODOO thus rls "integration" does NOT work anymore *)
1951 if UnparseC.term t =
1952 "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
1953 then () else error "integrate.sml 3rd integration in 7.27, integration";
1957 "----------- check probem type --------------------------";
1958 "----------- check probem type --------------------------";
1959 "----------- check probem type --------------------------";
1960 val thy = @{theory Integrate};
1961 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
1963 Find =["antiDerivative F_F"],
1965 Relate=[]}:string ppc;
1966 val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
1967 val t1 = (Thm.term_of o hd) chkmodel;
1968 val t2 = (Thm.term_of o hd o tl) chkmodel;
1969 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
1970 case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
1971 | _ => error "integrate.sml: Integrate.antiDerivative ???";
1974 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
1976 Find =["antiDerivativeName F_F"],
1978 Relate=[]}:string ppc;
1979 val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
1980 val t1 = (Thm.term_of o hd) chkmodel;
1981 val t2 = (Thm.term_of o hd o tl) chkmodel;
1982 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
1983 case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
1984 | _ => error "integrate.sml: Integrate.antiDerivativeName";
1987 "----- compare 'Find's from problem, script, formalization -------";
1988 val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
1989 val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
1990 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
1991 val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
1992 val [_,_, F2_] = formal_args sc;
1993 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
1995 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
1996 $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
1997 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
1998 if F1_type = F3_type then ()
1999 else error "integrate.sml: unequal types in find's";
2001 Test_Tool.show_ptyps();
2002 val pbl = Problem.from_store ["integrate", "function"];
2003 case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
2004 | _ => error "integrate.sml: Integrate.Integrate ???";
2008 "----------- me method [diff,integration] ---------------";
2009 "----------- me method [diff,integration] ---------------";
2010 "----------- me method [diff,integration] ---------------";
2011 (*exp_CalcInt_No- 1.xml*)
2012 val p = e_pos'; val c = [];
2013 "----- step 0: returns nxt = Model_Problem ---";
2014 val (p,_,f,nxt,_,pt) =
2016 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
2017 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
2018 "----- step 1: returns nxt = Add_Given \"functionTerm (x \<up> 2 + 1)\" ---";
2019 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
2020 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
2021 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2022 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
2023 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2024 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
2025 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2026 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
2027 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2028 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
2029 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2030 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
2031 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2032 case nxt of (Apply_Method ["diff", "integration"]) => ()
2033 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
2034 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
2035 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2036 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2037 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2038 if f2str f = "c + x + 1 / 3 * x \<up> 3" then ()
2039 else error "integrate.sml -- me method [diff,integration] -- end";
2043 "----------- autoCalculate [diff,integration] -----------";
2044 "----------- autoCalculate [diff,integration] -----------";
2045 "----------- autoCalculate [diff,integration] -----------";
2048 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
2049 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
2052 autoCalculate 1 CompleteCalc;
2053 val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
2054 val (Form t,_,_) = ME_Misc.pt_extract (pt, p);
2055 if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
2056 else error "integrate.sml -- interSteps [diff,integration] -- result";
2060 "----------- me method [diff,integration,named] ---------";
2061 "----------- me method [diff,integration,named] ---------";
2062 "----------- me method [diff,integration,named] ---------";
2063 (*exp_CalcInt_No- 2.xml*)
2064 val fmz = ["functionTerm (x \<up> 2 + (1::real))",
2065 "integrateBy x", "antiDerivativeName F"];
2067 ("Integrate",["named", "integrate", "function"],
2068 ["diff", "integration", "named"]);
2069 val p = e_pos'; val c = [];
2070 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2071 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2072 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2073 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
2074 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2075 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2076 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2077 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
2078 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2079 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2080 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2081 if f2str f = "F x = c + x + 1 / 3 * x \<up> 3" then()
2082 else error "integrate.sml: method [diff,integration,named]";
2086 "----------- me met [diff,integration,named] Biegelinie.Q";
2087 "----------- me met [diff,integration,named] Biegelinie.Q";
2088 "----------- me met [diff,integration,named] Biegelinie.Q";
2089 (*exp_CalcInt_No-3.xml*)
2090 val fmz = ["functionTerm (- q_0)",
2091 "integrateBy x", "antiDerivativeName Q"];
2093 ("Biegelinie",["named", "integrate", "function"],
2094 ["diff", "integration", "named"]);
2095 val p = e_pos'; val c = [];
2096 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2097 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2098 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2099 (*Error Tac Q not in ...*)
2100 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
2101 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2102 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2103 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2104 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
2105 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2106 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2108 if f2str f = "Q x = c + - q_0 * x" then()
2109 else error "integrate.sml: method [diff,integration,named] .Q";
2113 \<close> text \<open> (*-------^^^^^ integrate.sml------------vvv eqsystem.sml--------TOODOO-----------*)
2116 section \<open>======== check Knowledge/eqsystem.sml =============================================\<close>
2119 (* Title: Knowledge/eqsystem.sml
2120 Author: Walther Neuper 050826
2121 (c) due to copyright terms
2124 "-----------------------------------------------------------------";
2125 "table of contents -----------------------------------------------";
2126 "-----------------------------------------------------------------";
2127 "----------- occur_exactly_in ------------------------------------";
2128 "----------- problems --------------------------------------------";
2129 "----------- rewrite-order ord_simplify_System -------------------";
2130 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
2131 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
2132 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
2133 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
2134 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
2135 "----------- refine [linear,system]-------------------------------";
2136 "----------- refine [2x2,linear,system] search error--------------";
2137 "----------- me [EqSystem,normalise,2x2] -------------------------";
2138 "----------- me [linear,system] ..normalise..top_down_sub..-------";
2139 "----------- all systems from Biegelinie -------------------------";
2140 "----------- 4x4 systems from Biegelinie -------------------------";
2141 "-----------------------------------------------------------------";
2142 "-----------------------------------------------------------------";
2143 "-----------------------------------------------------------------";
2145 val thy = @{theory "EqSystem"};
2146 val ctxt = Proof_Context.init_global thy;
2148 "----------- occur_exactly_in ------------------------------------";
2149 "----------- occur_exactly_in ------------------------------------";
2150 "----------- occur_exactly_in ------------------------------------";
2151 val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
2152 val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
2154 if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
2155 then () else error "eqsystem.sml occur_exactly_in 1";
2157 if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
2158 then () else error "eqsystem.sml occur_exactly_in 2";
2160 if not (occur_exactly_in [TermC.str2term"c_2"] all t)
2161 then () else error "eqsystem.sml occur_exactly_in 3";
2163 val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
2164 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2165 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2166 if str = "[c, c_2] from [c, c_2,\n" ^
2167 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
2168 then () else error "eval_occur_exactly_in [c, c_2]";
2170 val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
2171 "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
2172 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2173 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
2174 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
2175 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
2177 val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
2178 \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
2179 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2180 if str = "[c_2] from [c, c_2,\n" ^
2181 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
2182 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
2184 val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
2185 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2186 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
2187 else error "eval_occur_exactly_in [c, c_2, c_3]";
2191 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
2192 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
2193 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
2194 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
2195 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
2197 "----------- problems --------------------------------------------";
2198 "----------- problems --------------------------------------------";
2199 "----------- problems --------------------------------------------";
2200 val t = TermC.str2term "Length [x+y=1,y=2] = 2";
2202 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
2203 [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})),
2204 (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})),
2205 Eval ("Groups.plus_class.plus", eval_binop "#add_"),
2206 Eval ("HOL.eq",eval_equal "#equal_")
2208 val SOME (t',_) = rewrite_set_ thy false testrls t;
2209 if UnparseC.term t' = "True" then ()
2210 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
2212 val SOME t = TermC.parse thy "solution LL";
2213 TermC.atomty (Thm.term_of t);
2214 val SOME t = TermC.parse thy "solution LL";
2215 TermC.atomty (Thm.term_of t);
2217 val t = TermC.str2term
2218 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
2220 val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
2221 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
2222 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
2223 assume flawed test setup hidden by "handle _ => ..."
2224 ERROR rewrite__set_ called with 'Erls' for '1 < 1'
2226 rewrite_set_ thy true
2227 (Rule_Set.append_rules "prls_" Rule_Set.empty
2228 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
2229 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
2230 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
2231 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
2232 Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
2234 if t = @{term True} then ()
2235 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
2236 broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
2239 "----------- rewrite-order ord_simplify_System -------------------";
2240 "----------- rewrite-order ord_simplify_System -------------------";
2241 "----------- rewrite-order ord_simplify_System -------------------";
2242 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
2243 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
2244 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
2245 TermC.str2term"c * x") then ()
2246 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
2248 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
2249 TermC.str2term"c_2") then ()
2250 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
2252 if ord_simplify_System false thy [] (TermC.str2term"c * x",
2253 TermC.str2term"c_2") then ()
2254 else error "integrate.sml, (c * x) < (c_2) not#3";
2256 "--- mult.commute ---";
2257 if ord_simplify_System false thy [] (TermC.str2term"x * c",
2258 TermC.str2term"c * x") then ()
2259 else error "integrate.sml, (x * c) < (c * x) not#4";
2261 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
2262 TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
2263 then () else error "integrate.sml, (. * .) < (. * .) not#5";
2265 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
2266 TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
2267 then () else error "integrate.sml, (. * .) < (. * .) not#6";
2271 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
2272 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
2273 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
2274 val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
2275 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
2276 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
2277 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
2278 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
2280 UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = - 0 + c_2]"
2281 \<close> text \<open>(* TOODOO: simplify_System_parenthesized \<longrightarrow> - 0 + c_4 ^^^^^^^^^^*)
2282 (* inhertited errors -----------------------------------------------------------------------\\* )
2283 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
2284 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
2286 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
2287 if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
2288 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
2290 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
2291 if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
2292 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
2294 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
2295 val SOME (t,_) = rewrite_set_ thy true order_system t;
2296 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
2297 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
2298 ( * inhertited errors -----------------------------------------------------------------------//*)
2300 \<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
2301 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
2302 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
2303 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
2304 val thy = @ {theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
2306 TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
2307 \ - 1 * q_0 / 24 * 0 \<up> 4),\
2308 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
2309 \ - 1 * q_0 / 24 * L \<up> 4)]";
2310 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
2311 if UnparseC.term t =
2312 "[0 = c_2,\n 0 = (24 * c_2 * EI + 24 * L * c * EI + L \<up> 4 * q_0) / (24 * EI)]"
2313 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
2315 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
2316 if UnparseC.term t = (*"[0 = 0 / EI + c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
2317 "[0 = c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"
2318 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
2320 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
2321 if UnparseC.term t = (*"[c_2 = 0 + - 1 * (0 / EI),\n L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
2322 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"
2323 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
2325 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
2326 if UnparseC.term t = (*"[c_2 = 0 / EI, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
2327 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
2328 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
2330 val xxx = rewrite_set_ thy true order_system t;
2332 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
2336 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
2337 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
2338 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
2339 val e1__ = TermC.str2term "c_2 = 77";
2340 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
2341 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
2342 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
2343 val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
2344 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
2345 else error "eqsystem.sml top_down_substitution,2x2] subst";
2349 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
2350 if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
2351 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
2354 val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
2355 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
2356 else error "eqsystem.sml top_down_substitution,2x2] isolate";
2359 val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
2360 val SOME (t,_) = rewrite_set_ thy true order_system t;
2361 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
2362 else error "eqsystem.sml top_down_substitution,2x2] order_system";
2365 if not (ord_simplify_System
2367 (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
2368 TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
2369 then () else error "eqsystem.sml, order_result rew_ord";
2373 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
2374 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
2375 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
2376 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
2377 val t = TermC.str2term (
2378 "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
2379 "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
2380 "c + c_2 + c_3 + c_4 = 0, " ^
2381 "c_2 + c_3 + c_4 = 0]");
2383 val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
2384 (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
2385 (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
2386 (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
2388 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
2391 "[0 = - 0 + c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
2392 \<close> text \<open> (* ^^^^^^- TOODOO: simplify_System_parenthesized \<longrightarrow> - 0 + c_4*)
2393 (* inhertited errors -----------------------------------------------------------------------\\* )
2394 if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4), c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
2395 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
2397 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
2398 if UnparseC.term t = "[c_4 = 0, \
2399 \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
2400 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
2401 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
2403 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
2404 if UnparseC.term t = "[c_4 = 0,\
2405 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
2406 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
2407 \ c_2 + (c_3 + c_4) = 0]"
2408 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
2410 val SOME (t,_) = rewrite_set_ thy true order_system t;
2411 if UnparseC.term t = "[c_4 = 0,\
2412 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
2413 \ c_2 + (c_3 + c_4) = 0,\n\
2414 \ c + (c_2 + (c_3 + c_4)) = 0]"
2415 then () else error "eqsystem.sml rewrite in 4x4 order_system";
2416 ( * inhertited errors -----------------------------------------------------------------------//*)
2419 "----------- refine [linear,system]-------------------------------";
2420 "----------- refine [linear,system]-------------------------------";
2421 "----------- refine [linear,system]-------------------------------";
2423 ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
2424 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
2425 "solveForVars [c, c_2]", "solution LL"];
2427 (*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR", "system"]" caused an error...*)
2428 "~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
2429 "~~~~~ fun refin', args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
2430 ((rev o tl) pblID, fmz, [(*match list*)],
2431 ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
2432 val {thy, ppc, where_, prls, ...} = py ;
2433 "~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
2434 val ctxt = Proof_Context.init_global thy;
2435 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
2436 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
2437 (_, _::_) => (Free (v,T)::get_vars vs)
2438 | (_, [] ) => get_vars vs) (*filter out nums as long as
2439 we have Free ("123",_)*)
2441 t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
2442 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
2443 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
2444 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
2445 val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
2446 val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
2447 val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
2448 val t = nth 2 fmz; t = "solveForVars [c, c_2]";
2449 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
2450 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
2451 val t = nth 3 fmz; t = "solution LL";
2452 (*(Syntax.read_term ctxt t);
2453 Type unification failed: Clash of types "real" and "_ list"
2454 Type error in application: incompatible operand type
2456 Operator: solution :: bool list \<Rightarrow> toreall
2457 Operand: L :: real ========== L was already present in equalities ========== *)
2460 "===== case 1 =====";
2461 val matches = Refine.refine fmz ["LINEAR", "system"];
2463 [M_Match.Matches (["LINEAR", "system"], _),
2464 M_Match.Matches (["2x2", "LINEAR", "system"], _),
2465 M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
2466 M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
2467 {Find = [Correct "solution LL"],
2471 "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
2472 Correct "solveForVars [c, c_2]"],
2474 Relate = []})] => ()
2475 | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
2478 "===== case 2 =====";
2479 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
2480 "solveForVars [c, c_2]", "solution LL"];
2481 val matches = Refine.refine fmz ["LINEAR", "system"];
2482 case matches of [_,_,
2484 (["triangular", "2x2", "LINEAR", "system"],
2485 {Find = [Correct "solution LL"],
2488 [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
2489 Correct "solveForVars [c, c_2]"],
2491 "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
2493 "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
2494 Relate = []})] => ()
2495 | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
2498 (*WN051014-----------------------------------------------------------------------------------\\
2499 the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
2500 didn't work anymore; we investigated in these steps:(**)
2501 val fmz = ["equalities [(c_2::real) = 0, L * (c::real) + c_2 = q_0 * L \<up> 2 / 2]",
2502 "solveForVars [(c::real), (c_2::real)]", "solution LL"];
2503 val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
2505 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
2506 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
2507 val t = TermC.str2term ("[(c::real), (c_2::real)] from [(c::real), (c_2::real)] occur_exactly_in NTH 2" ^
2508 "[(c_2::real) = 0, L * (c::real) + c_2 = q_0 * L \<up> 2 / 2]");
2509 Rewrite.trace_on := false; (*true false*)
2510 val SOME (t', _) = rewrite_set_ thy false prls_triangular t;
2512 ## try thm: NTH_CONS
2513 ### eval asms: 1 < 2 + - 1
2514 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
2515 nth_ (2 + - 1 + - 1) []
2516 #### rls: erls_prls_triangular on: 1 < 2 + - 1
2517 ##### try calc: op <'
2518 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
2520 ... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
2521 --------------------------------------------------------------------------------------------//*)
2524 "===== case 3: relaxed preconditions for triangular system =====";
2525 val fmz = ["equalities [L * q_0 = c, \
2526 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
2529 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
2530 (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
2531 probably exn thrown by fun declare_constraints
2532 /-------------------------------------------------------\
2533 Type unification failed
2534 Type error in application: incompatible operand type
2536 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
2537 Operand: [c_4] :: 'b list
2538 \-------------------------------------------------------/
2539 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
2540 case TermC.matches of
2541 [M_Match.Matches (["LINEAR", "system"], _),
2542 M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
2543 M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
2544 M_Match.Matches (["4x4", "LINEAR", "system"], _),
2545 M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
2546 M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
2547 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
2548 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
2550 "===== case 4 =====";
2551 val fmz = ["equalities [L * q_0 = c, \
2552 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
2555 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
2556 val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
2557 case TermC.matches of
2558 [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
2559 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
2560 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
2561 ============ inhibit exn WN120314 ==============================================*)
2564 "----------- Refine.refine [2x2,linear,system] search error--------------";
2565 "----------- Refine.refine [2x2,linear,system] search error--------------";
2566 "----------- Refine.refine [2x2,linear,system] search error--------------";
2567 (*didn't go into ["2x2", "LINEAR", "system"];
2568 we investigated in these steps:*)
2569 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
2570 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
2571 "solveForVars [c, c_2]", "solution LL"];
2572 Rewrite.trace_on := false; (*true false*)
2573 val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
2574 Rewrite.trace_on := false; (*true false*)
2575 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
2576 (*brought: 'False "length_ es_ = 2"'*)
2578 (*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
2579 (* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
2580 (rev ["LINEAR", "system"], fmz, [(*match list*)],
2581 ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
2583 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
2584 val it = "length_ (es_::real list) = (2::real)" : string
2586 =========================================================================\
2587 -------fun Problem.prep_input
2588 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
2589 ev:rls, ca: string option, metIDs:metID list)) =
2590 (EqSystem.thy, (["system"],
2591 [("#Given" ,["equalities es_", "solveForVars v_s"]),
2592 ("#Find" ,["solution ss___"](*___ is copy-named*))
2594 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
2595 SOME "solveSystem es_ v_s",
2598 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
2599 val equalities_es_ = "equalities es_" : string
2600 > val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
2601 > show_types:=true; UnparseC.term ii; show_types:=false;
2602 val it = "es_::bool list" : string
2603 ~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2605 > val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
2606 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
2608 =========================================================================/
2611 > (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
2613 (1 ,[1] ,true ,#Given ,Cor equalities
2614 [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
2615 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
2616 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
2617 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
2618 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
2620 > (writeln o pres2str) pre';
2622 (false, length_ es_ = 2),
2623 (true, length_ [c, c_2] = 2)]
2625 ----- fun match_oris':
2626 > (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
2627 > (writeln o pres2str) pre';
2630 ----- fun check in Pre_Conds.
2631 > (writeln o env2str) env;
2633 (es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
2634 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
2638 > val es_ = (fst o hd) env;
2639 val es_ = Free ("es_", "bool List.list") : Term.term
2641 > val pre1 = hd pres;
2644 *** Const (op =, [real, real] => bool)
2645 *** . Const (ListG.length_, real list => real)
2646 *** . . Free (es_, real list)
2647 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
2648 *** . Free (2, real)
2651 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
2652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2655 \<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
2656 "----------- me [EqSystem,normalise,2x2] -------------------------";
2657 "----------- me [EqSystem,normalise,2x2] -------------------------";
2658 "----------- me [EqSystem,normalise,2x2] -------------------------";
2659 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
2660 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
2661 "solveForVars [c, c_2]", "solution LL"];
2663 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
2664 ["EqSystem", "normalise", "2x2"]);
2665 val p = e_pos'; val c = [];
2666 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2667 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2668 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2669 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2670 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2671 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
2672 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
2674 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2675 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2676 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
2677 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2678 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2679 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2681 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
2682 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
2684 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2685 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2686 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2687 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2689 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
2690 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
2692 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2693 val PblObj {probl,...} = get_obj I pt [5];
2694 (writeln o (I_Model.to_string (ThyC.to_ctxt @ {theory Isac_Knowledge}))) probl;
2696 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
2697 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
2698 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
2700 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2701 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2702 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2703 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2704 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2705 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2706 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2707 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2709 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
2710 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
2711 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2712 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2713 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
2714 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
2717 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
2719 \<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
2720 "----------- me [linear,system] ..normalise..top_down_sub..-------";
2721 "----------- me [linear,system] ..normalise..top_down_sub..-------";
2722 "----------- me [linear,system] ..normalise..top_down_sub..-------";
2725 \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
2726 \ - 1 * q_0 / 24 * 0 \<up> 4),\
2727 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
2728 \ - 1 * q_0 / 24 * L \<up> 4)]",
2729 "solveForVars [c, c_2]", "solution LL"];
2731 ("Biegelinie",["LINEAR", "system"], ["no_met"]);
2732 val p = e_pos'; val c = [];
2733 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2734 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2735 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2736 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2737 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2738 case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
2739 | _ => error "eqsystem.sml [linear,system] specify b";
2740 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2741 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2742 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2743 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2744 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2745 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2747 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
2748 then () else error "eqsystem.sml me simpl. before SubProblem b";
2750 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
2751 | _ => error "eqsystem.sml me [linear,system] SubProblem b";
2753 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2754 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2755 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2756 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2758 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
2759 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
2761 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2762 val PblObj {probl,...} = get_obj I pt [5];
2763 (writeln o (I_Model.to_string (ThyC.to_ctxt @ {theory Isac_Knowledge}))) probl;
2765 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
2766 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
2767 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
2769 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2770 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2771 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2772 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2773 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2774 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2775 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2776 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2778 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
2779 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
2780 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2781 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
2783 if f2str f = "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"
2784 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
2787 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
2791 "----------- all systems from Biegelinie -------------------------";
2792 "----------- all systems from Biegelinie -------------------------";
2793 "----------- all systems from Biegelinie -------------------------";
2794 val thy = @{theory Isac_Knowledge}
2796 [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
2797 (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
2802 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
2803 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
2804 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
2807 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
2808 ##7.27## ordered substs
2810 c c_2 c_3 c_4 c c_2 1->2: c
2812 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
2813 val t = TermC.str2term
2815 "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
2817 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
2818 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
2819 if UnparseC.term t =
2820 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
2821 then () else error "Bsp 7.27";
2823 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
2824 val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
2825 val NONE = rewrite_set_ thy false norm_Rational t;
2827 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
2828 if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
2829 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
2831 "--- isolate_bdvs_4x4";
2833 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
2835 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
2837 val SOME (t,_) = rewrite_set_ thy false order_system t;
2841 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
2843 CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
2844 ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
2846 "Randbedingungen [y L = 0, y' L = 0]",
2847 "FunktionsVariable x"],
2848 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
2849 ["Biegelinien", "AusMomentenlinie"]))];
2852 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
2858 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
2859 "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
2860 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
2863 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
2864 ##7.69## ordered subst 2x2
2866 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
2868 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
2869 val t = TermC.str2term
2870 ("[0 = c_4 + 0 / (- 1 * EI), " ^
2871 "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
2872 "0 = c_3 + 0 / (- 1 * EI), " ^
2873 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
2878 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
2879 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
2880 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
2883 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
2888 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
2891 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
2892 val t = TermC.str2term
2894 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
2897 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
2898 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
2899 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
2900 if UnparseC.term t =
2901 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
2902 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
2905 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
2906 if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
2907 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
2909 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
2910 if UnparseC.term t =
2911 "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
2912 " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
2913 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
2915 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
2917 UnparseC.term t = "[c = - 0 + - 1 * L * q_0 / - 1, " ^
2918 (*^^^^^^*) "L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"
2919 \<close> text \<open> (*TOODOO simplify_System_parenthesized: \<longrightarrow> - 0 + - 1 * L * q_0 / - 1 *)
2921 if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"
2922 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
2925 val SOME (t, _) = rewrite_set_ thy false order_system t;
2928 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
2929 \<close> ML \<open> (*TOODOO order_system: \<longrightarrow> c_4 = 0, c_3 = 0 *)
2931 if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
2932 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
2936 "----- 7.70 with met normalise: ";
2937 val fmz = ["equalities" ^
2939 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
2941 "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
2942 val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
2943 val p = e_pos'; val c = [];
2946 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
2947 in next but one test below the same type error.
2948 /-------------------------------------------------------\
2949 Type unification failed
2950 Type error in application: incompatible operand type
2952 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
2953 Operand: [c_4] :: 'b list
2954 \-------------------------------------------------------/
2956 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2957 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2958 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2959 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2960 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2961 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
2962 | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
2963 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2965 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
2966 (*-----------------------------------vvvWN080102 Exception- Match raised
2967 since associate Rewrite .. Rewrite_Set
2968 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2970 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2971 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2973 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2974 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2975 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2976 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2977 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
2978 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
2979 --------------------------------------------------------------------------*)
2980 ============ inhibit exn WN120314 ==============================================*)
2983 "----- 7.70 with met top_down_: me";
2985 "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
2986 "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
2988 ("Biegelinie",["LINEAR", "system"],["no_met"]);
2989 val p = e_pos'; val c = [];
2990 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2991 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2992 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2993 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2994 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2995 case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
2996 | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
2997 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2998 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2999 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3000 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3001 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3002 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3003 if p = ([], Res) andalso
3004 (* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
3005 f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
3006 then () else error "eqsystem.sml: 7.70 with met top_down_: me";
3011 CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
3012 "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
3013 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
3014 "AbleitungBiegelinie dy"],
3015 ("Biegelinie", ["Biegelinien"],
3016 ["IntegrierenUndKonstanteBestimmen2"] ))];
3019 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
3020 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
3021 c c_2 |c c_2 |1' |1': c c_2 |
3022 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
3023 c c_2 c_3 c_4 | c_4 |3' | |
3024 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
3025 val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
3026 \ 0 = c_4 + 0 / (- 1 * EI), \
3027 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
3028 \ 0 = c_3 + 0 / (- 1 * EI)]";
3030 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
3032 CalcTree [(["Traegerlaenge L",
3033 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
3035 "Randbedingungen [y 0 = (0::real), y L = 0]",
3036 "FunktionsVariable x"],
3037 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
3038 ["Biegelinien", "AusMomentenlinie"]))];
3041 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
3045 "------- Bsp 7.72b";
3047 CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
3048 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
3049 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
3050 "AbleitungBiegelinie dy"],
3051 ("Biegelinie", ["Biegelinien"],
3052 ["IntegrierenUndKonstanteBestimmen2"] ))];
3055 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
3056 ##7.72b## |ord. |subst.singles |ord.triang.
3058 c c_2 | |1:c_2 -> 2':c |c_2 c
3060 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
3061 val t = TermC.str2term"[0 = c_2, \
3062 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
3063 \ 0 = c_4 + 0 / (- 1 * EI), \
3064 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
3066 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
3068 CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
3070 "Randbedingungen [y L = 0, y' L = 0]",
3071 "FunktionsVariable x"],
3072 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
3073 ["Biegelinien", "AusMomentenlinie"]))];
3076 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
3080 "----------- 4x4 systems from Biegelinie -------------------------";
3081 "----------- 4x4 systems from Biegelinie -------------------------";
3082 "----------- 4x4 systems from Biegelinie -------------------------";
3083 (*STOPPED.WN08?? replace this test with 7.70 *)
3085 val fmz = ["equalities \
3087 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
3089 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
3090 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
3092 ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
3093 ["EqSystem", "normalise", "4x4"]);
3094 val p = e_pos'; val c = [];
3095 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3096 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3097 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3098 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3099 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3100 "------------------------------------------- Apply_Method...";
3101 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3103 \ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
3105 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
3106 (*vvvWN080102 Exception- Match raised
3107 since associate Rewrite .. Rewrite_Set
3108 "------------------------------------------- simplify_System_parenthesized...";
3109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3111 \ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
3112 \ (4 * L \<up> 3 * c / (- 24 * EI) + \
3113 \ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
3114 \ (L * c_3 + c_4))), \
3116 \ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
3117 (*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
3118 "------------------------------------------- isolate_bdvs...";
3119 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3121 \ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
3123 \ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
3124 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3126 ---------------------------------------------------------------------*)
3131 section \<open>===================================================================================\<close>
3138 section \<open>===================================================================================\<close>
3145 section \<open>code for copy & paste ===============================================================\<close>
3147 "~~~~~ fun xxx , args:"; val () = ();
3148 "~~~~~ and xxx , args:"; val () = ();
3149 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
3150 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);