1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
2 Author: Walther Neuper 101001
3 (c) copyright due to license terms.
5 Isac's tests are organised parallel to sources:
6 $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
8 $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
9 $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
11 Note, that only the first error in a file is shown here.
14 section \<open>Notes on running tests\<close>
15 subsection \<open>Switch between running tests and updating code\<close>
17 Isac encapsulates code as much as possible in structures without open.
18 This policy conflicts with those tests, which go into functions to details
19 not declared in the signatures.
21 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
23 Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
24 if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
25 This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
26 A model is in the repository at ~~/etc/preferences.
27 These preferences have drawbacks, however:
28 * they claim more memory such that Isabelle instances canNOT run in parallel.
29 * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
31 So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
32 From time to time full testing in Test_Isac.thy is recommended. For that purpose
33 * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
35 \\******************* don't forget to re-set defaults BEFORE updating code *******************//
37 Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
38 ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
41 section \<open>Run the tests\<close>
43 * say "OK" to the popup asking for theories to be loaded
44 * watch the <Theories> window for errors in the "imports" below
48 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
49 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
50 and find out, which ML_file or *.thy causes an error (might be ONLY one).
51 Also backup files (#* ) recognised by jEdit cause this trouble *)
52 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
53 (* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
54 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
55 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
56 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
57 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
58 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
59 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
60 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
61 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
62 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
63 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
64 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
65 ADDTESTS/------------------------------------------- see end of tests *)
66 (*/~~~ these work directly from Pure, but create problems here ..
67 "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
68 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
69 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
70 "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
71 "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
72 \~~~ .. these work independently, but create problems here *)
73 (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
74 (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
75 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
76 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
77 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
78 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
80 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
81 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*)
82 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
83 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
88 declare [[ML_print_depth = 20]]
90 ML \<open>open ML_System\<close>
94 open Test_Code; Test_Code.init_calc @{context};
95 open LItool; arguments_from_model;
103 open Error_Pattern_Def;
105 open Ctree; append_problem;
111 open Auto_Prog; rule2stac;
118 open Solve; (* NONE *)
119 open ContextC; transfer_asms_from_to;
120 open Tactic; (* NONE *)
123 open P_Model; (* NONE *)
128 open Rule_Set; Sequence;
138 "~~~~~ fun xxx , args:"; val () = ();
139 "~~~~~ and xxx , args:"; val () = ();
140 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
141 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
143 ^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)
144 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
145 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
146 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
147 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
157 KEStore_Elems.set_ref_thy @{theory};
158 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
161 section \<open>trials with Isabelle's functions\<close>
162 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
163 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
164 ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
165 ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
166 ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
167 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
169 section \<open>test ML Code of isac\<close>
170 subsection \<open>basic code first\<close>
171 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
172 ML_file "BaseDefinitions/base-definitions.sml"
173 ML_file "BaseDefinitions/libraryC.sml"
174 ML_file "BaseDefinitions/rule-def.sml"
175 ML_file "BaseDefinitions/eval-def.sml"
176 ML_file "BaseDefinitions/rewrite-order.sml"
177 ML_file "BaseDefinitions/theoryC.sml"
178 ML_file "BaseDefinitions/rule.sml"
179 ML_file "BaseDefinitions/thmC-def.sml"
180 ML_file "BaseDefinitions/error-fill-def.sml"
181 ML_file "BaseDefinitions/rule-set.sml"
182 ML_file "BaseDefinitions/check-unique.sml"
183 (*called by Know_Store..*)
184 ML_file "BaseDefinitions/calcelems.sml"
185 ML_file "BaseDefinitions/termC.sml"
186 ML_file "BaseDefinitions/substitution.sml"
187 ML_file "BaseDefinitions/contextC.sml"(*sometimes needs separation into ML blocks for evaluation*)
188 ML_file "BaseDefinitions/environment.sml"
189 (** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
190 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
191 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
193 ML_file "ProgLang/calculate.sml"
194 ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
195 ML_file "ProgLang/listC.sml"
196 ML_file "ProgLang/prog_expr.sml"
197 ML_file "ProgLang/program.sml"
198 ML_file "ProgLang/prog_tac.sml"
199 ML_file "ProgLang/tactical.sml"
200 ML_file "ProgLang/auto_prog.sml"
201 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
202 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
204 subsection \<open>basic functionality on simple example first\<close>
205 ML_file "Minisubpbl/000-comments.sml"
206 ML_file "Minisubpbl/100-init-rootpbl.sml"
207 ML_file "Minisubpbl/150-add-given.sml"
208 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
209 ML_file "Minisubpbl/200-start-method.sml"
210 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
211 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
212 ML_file "Minisubpbl/300-init-subpbl.sml"
213 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
214 ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
215 ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
216 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
217 ML_file "Minisubpbl/500-met-sub-to-root.sml"
218 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
219 ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
220 ML_file "Minisubpbl/600-postcond.sml"
221 ML_file "Minisubpbl/700-interSteps.sml"
222 ML_file "Minisubpbl/710-interSteps-short.sml"
223 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
224 ML_file "Minisubpbl/790-complete.sml"
225 ML_file "Minisubpbl/800-append-on-Frm.sml"
227 subsection \<open>further functionality alongside batch build sequence\<close>
228 ML_file "MathEngBasic/thmC.sml"
229 ML_file "MathEngBasic/rewrite.sml"
230 ML_file "MathEngBasic/tactic.sml"
231 ML_file "MathEngBasic/ctree.sml"
232 ML_file "MathEngBasic/calculation.sml"
234 ML_file "Specify/formalise.sml"
235 ML_file "Specify/o-model.sml"
236 ML_file "Specify/i-model.sml"
237 ML_file "Specify/pre-conditions.sml"
238 ML_file "Specify/p-model.sml"
239 ML_file "Specify/m-match.sml"
240 ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
241 ML_file "Specify/test-out.sml"
242 ML_file "Specify/specify-step.sml"
243 ML_file "Specify/specification.sml"
244 ML_file "Specify/cas-command.sml"
245 ML_file "Specify/p-spec.sml"
246 ML_file "Specify/specify.sml"
247 ML_file "Specify/step-specify.sml"
249 ML_file "Interpret/istate.sml"
250 ML_file "Interpret/sub-problem.sml"
251 ML_file "Interpret/error-pattern.sml"
252 ML_file "Interpret/li-tool.sml"
253 ML_file "Interpret/lucas-interpreter.sml"
254 ML_file "Interpret/step-solve.sml"
256 ML_file "MathEngine/me-misc.sml"
257 ML_file "MathEngine/fetch-tactics.sml"
258 ML_file "MathEngine/solve.sml"
259 ML_file "MathEngine/step.sml"
260 ML_file "MathEngine/mathengine-stateless.sml"
261 ML_file "MathEngine/messages.sml"
262 ML_file "MathEngine/states.sml"
264 ML_file "BridgeLibisabelle/thy-present.sml"
265 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
266 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
267 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
268 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
269 ML_file "BridgeLibisabelle/interface.sml"
270 ML_file "BridgeJEdit/parseC.sml"
271 ML_file "BridgeJEdit/preliminary.sml"
272 ML_file "BridgeJEdit/vscode-example.sml"
274 ML_file "Knowledge/delete.sml"
275 ML_file "Knowledge/descript.sml"
276 ML_file "Knowledge/simplify.sml"
277 ML_file "Knowledge/poly-1.sml"
278 ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
279 ML_file "Knowledge/gcd_poly_ml.sml"
280 ML_file "Knowledge/rational-1.sml"
281 ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)
282 ML_file "Knowledge/equation.sml"
283 ML_file "Knowledge/root.sml"
284 ML_file "Knowledge/lineq.sml"
285 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
286 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered----Test_Isac_Short*)
287 ML_file "Knowledge/rootrat.sml"
288 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
289 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
290 ML_file "Knowledge/polyeq-1.sml"
291 ML_file "Knowledge/polyeq-2.sml" (*Test_Isac_Short*)
292 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
293 ML_file "Knowledge/calculus.sml"
294 ML_file "Knowledge/trig.sml"
295 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
296 ML_file "Knowledge/diff.sml"
297 ML_file "Knowledge/integrate.sml"
298 ML_file "Knowledge/eqsystem-1.sml"
299 ML_file "Knowledge/eqsystem-1a.sml"
300 ML_file "Knowledge/eqsystem-2.sml"
301 ML_file "Knowledge/test.sml"
302 ML_file "Knowledge/polyminus.sml"
303 ML_file "Knowledge/vect.sml"
304 ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
305 ML_file "Knowledge/biegelinie-1.sml"
306 ML_file "Knowledge/biegelinie-2.sml" (*Test_Isac_Short*)
307 ML_file "Knowledge/biegelinie-3.sml" (*Test_Isac_Short*)
308 ML_file "Knowledge/biegelinie-4.sml"
309 ML_file "Knowledge/algein.sml"
310 ML_file "Knowledge/diophanteq.sml"
311 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
312 ML_file "Knowledge/inssort.sml"
313 ML_file "Knowledge/isac.sml"
314 ML_file "Knowledge/build_thydata.sml"
316 ML_file "Test_Code/test-code.sml"
318 section \<open>further tests additional to src/.. files\<close>
319 ML_file "BridgeLibisabelle/use-cases.sml"
323 (* Title: tests the interface of isac's SML-kernel in accordance to
324 java-tests/isac.bridge.
325 Author: Walther Neuper
326 (c) copyright due to lincense terms.
328 Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.
329 Some tests are outcommented since "eliminate ThmC.numerals_to_Free";
330 these are considered irrelevant for Isabelle/Isac.
332 WN050707 ... if true, the test ist marked with a \label referring
333 to the same UC in isac-docu.tex as the JUnit testcase.
334 WN120210?not ME: added some labels, which are not among the above,
335 repaired lost \label (s).
337 theory Test_Some imports Isac.Build_Thydata begin
338 ML {* KEStore_Elems.set_ref_thy @{theory};
339 fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
340 ML_file "Frontend/use-cases.sml"
343 "--------------------------------------------------------";
344 "table of contents --------------------------------------";
345 "--------------------------------------------------------";
346 "within struct ------------------------------------------";
347 "--------------------------------------------------------";
348 "--------- encode ^ -> ^^ ------------------------------";
349 "--------------------------------------------------------";
350 "exported from struct -----------------------------------";
351 "--------------------------------------------------------";
352 (*"--------- empty rootpbl --------------------------------";*)
353 "--------- solve_linear as rootpbl FE -------------------";
354 "--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
355 "--------- miniscript with mini-subpbl ------------------";
356 "--------- mini-subpbl AUTOCALCULATE Steps 1 ------------";
357 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
358 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
359 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
360 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
361 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
362 "--------- setContext..Thy ------------------------------";
363 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
364 "--------- rat-eq + subpbl: no_met, NO solution dropped - WITH fun me IN test/../solve.sml";
365 "--------- tryMatchProblem, tryRefineProblem ------------";
366 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
367 "--------- maximum-example, UC: Modeling an example -----";
368 "--------- solve_linear from pbl-hierarchy --------------";
369 "--------- solve_linear as in an algebra system (CAS)----";
370 "--------- interSteps: on 'miniscript with mini-subpbl' -";
371 "--------- getTactic, fetchApplicableTactics ------------";
372 "--------- getAssumptions, getAccumulatedAsms -----------";
373 "--------- arbitrary combinations of steps --------------";
374 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
375 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
376 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
377 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
378 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
379 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
380 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
381 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
382 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
383 "--------- UC errpat add-fraction, fillpat by input --------------";
384 "--------- UC errpat, fillpat step to Rewrite --------------------";
385 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
386 "--------------------------------------------------------";
388 "within struct ---------------------------------------------------";
389 "within struct ---------------------------------------------------";
390 "within struct ---------------------------------------------------";
391 (*==================================================================
393 ==================================================================*)
394 "exported from struct --------------------------------------------";
395 "exported from struct --------------------------------------------";
396 "exported from struct --------------------------------------------";
399 (*------------ set at startup of the Kernel ----------------------*)
400 States.reset (); (*resets all state information in Kernel *)
401 (*----------------------------------------------------------------*)
403 (*---------------------------------------------------- postpone to Outer_Syntax..Example -----
404 "--------- empty rootpbl --------------------------------";
405 "--------- empty rootpbl --------------------------------";
406 "--------- empty rootpbl --------------------------------";
407 CalcTree @{context} [([], ("", [], []))];
410 refFormula 1 (States.get_pos 1 1);
411 (*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
413 ------------------------------------------------------ postpone to Outer_Syntax..Example -----*)
415 "--------- solve_linear as rootpbl FE -------------------";
416 "--------- solve_linear as rootpbl FE -------------------";
417 "--------- solve_linear as rootpbl FE -------------------";
420 CalcTree @{context} (*start of calculation, return No.1*)
421 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
423 ["LINEAR", "univariate", "equation", "test"],
424 ["Test", "solve_linear"]))];
425 Iterator 1; (*create an active Iterator on CalcTree @{context} No.1*)
427 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree @{context} No.1*);
428 refFormula 1 (States.get_pos 1 1) (*gets CalcHead; model is still empty*);
431 (*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
432 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
433 autoCalculate 1 (Steps 1);
434 refFormula 1 (States.get_pos 1 1) (*model contains descriptions for all items*);
435 autoCalculate 1 (Steps 1);
436 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
437 (*2*) fetchProposedTactic 1;
438 setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
439 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*equality added*);
441 (*3*) fetchProposedTactic 1;
442 setNextTactic 1 (Add_Given "solveFor x");
443 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
445 (*4*) fetchProposedTactic 1;
446 setNextTactic 1 (Add_Find "solutions L");
447 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
449 (*5*) fetchProposedTactic 1;
450 setNextTactic 1 (Specify_Theory "Test");
451 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
452 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
454 (*6*) fetchProposedTactic 1;
455 setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
456 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
457 (*-------------------------------------------------------------------------*)
458 (*7*) fetchProposedTactic 1;
459 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
461 setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
462 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
464 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
465 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
467 (*-------------------------------------------------------------------------*)
468 (*8*) fetchProposedTactic 1;
469 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
471 (*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
472 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
473 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
474 SpecificationC.is_complete ptp;
475 References.are_complete ptp;
477 (*8*) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*<---------------------- orig. test code*)
479 val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
480 (*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
481 andalso Istate.string_of (get_istate_LI pt p)
482 = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
483 then () else error "refFormula = 1 + - 1 * 2 + x = 0 changed";
484 (*-------------------------------------------------------------------------*)
486 (*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)
487 (*+\\------------------------------------------ isa == REP -----------------------------------//* )
488 (*+//========================================== isa <> REP (1) ===============================\\*)
489 (*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
491 "~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
492 val ((pt'''''_', _), _) = States.get_calc cI
493 val ip'''''_' = States.get_pos cI 1;
495 val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
496 (*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
497 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
499 (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
500 Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
501 if Istate.string_of istate
502 = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
503 then () else error "from Step.by_tactic return --- changed 1";
505 if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
506 = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
507 then () else error "from Step.by_tactic return --- changed 2";
508 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
510 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
511 val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
512 (*if*) Tactic.for_specify' m; (*false*)
514 Step_Solve.by_tactic m (pt, p);
515 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
516 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
517 val thy' = get_obj g_domID pt (par_pblobj pt p);
518 val (is, sc) = LItool.resume_prog (p,p_) pt;
519 val Safe_Step (istate, _, tac) =
520 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
522 (*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
523 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
524 (*+*)if Istate.string_of istate
525 (*+isa*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
526 then case m of Rewrite_Set_Inst' _ => ()
527 else error "from locate_input_tactic return --- changed";
529 val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
530 "~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
531 (*\\=========================================== isa <> REP (1) ===============================//*)
532 (*//=========================================== isa <> REP (2) ===============================\\*)
533 (*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
534 ( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)
536 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
537 val pold = States.get_pos cI 1;
538 val xxx = (States.get_calc cI);
539 (*isa*) val (**)xxxx(**) (**) = (**)
540 (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
541 "~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
542 (*if*) s <= 1; (*then*)
543 (*val (str, (_, c', ptp)) =*)
546 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
548 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
549 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
550 (*+*)if pos' = ([1], Res) andalso Istate.string_of istate
551 = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
552 then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
554 val pIopt = get_pblID (pt,ip);
555 (*if*) ip = ([], Pos.Res);(*else*)
556 val (_::_) = (*case*) tacis (*of*);
557 (*isa==REP*) (*if*) ip = p;(*then*)
558 (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
559 (*//------------------------------------- final test -----------------------------------------\\*)
560 val ("ok", [], ptp as (pt, p)) = xxxx;
562 if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> \<up> \<up> \<up> \<up> ^*)
563 (*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
564 then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
566 "~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
567 (*\\=========================================== isa <> REP (2) ===============================//*)
569 (*10*) fetchProposedTactic 1;
570 setNextTactic 1 (Rewrite_Set "Test_simplify");
571 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
573 (*11*) fetchProposedTactic 1;
574 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
575 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
577 (*======= final test ==================================================*)
578 val ((pt,_),_) = States.get_calc 1;
579 val ip = States.get_pos 1 1;
581 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
582 (*exception just above means: 'ModSpec' has been returned: error anyway*)
583 if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
584 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
587 "--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
588 "--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
589 "--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
590 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
591 (*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
593 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
595 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
597 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
598 (*getAssumption 1 ([1],Res); TODO.WN041217*)
599 moveActiveDown 1 ; refFormula 1 ([2],Res);
600 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
604 if States.get_pos 1 1 = ([2], Res) then () else
605 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
606 moveActiveDown 1; refFormula 1 ([], Res);
607 if States.get_pos 1 1 = ([], Res) then () else
608 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
609 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
611 ------------------------------------------------------------------------------------------------*)
613 "--------- miniscript with mini-subpbl ------------------";
614 "--------- miniscript with mini-subpbl ------------------";
615 "--------- miniscript with mini-subpbl ------------------";
616 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
617 "=== this sequence of fun-calls resembles fun me ===";
618 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
619 ("Test", ["sqroot-test", "univariate", "equation", "test"],
620 ["Test", "squ-equ-test-subpbl1"]))];
624 refFormula 1 (States.get_pos 1 1);
625 fetchProposedTactic 1;
626 setNextTactic 1 (Model_Problem);
627 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*gets ModSpec;model is still empty*)
629 fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
630 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
631 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
633 fetchProposedTactic 1;
634 setNextTactic 1 (Add_Given "solveFor x");
635 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
637 fetchProposedTactic 1;
638 setNextTactic 1 (Add_Find "solutions L");
639 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
641 fetchProposedTactic 1;
642 setNextTactic 1 (Specify_Theory "Test");
643 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
645 fetchProposedTactic 1;
646 setNextTactic 1 (Specify_Problem
647 ["sqroot-test", "univariate", "equation", "test"]);
648 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
649 "1-----------------------------------------------------------------";
651 fetchProposedTactic 1;
652 setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
653 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
655 fetchProposedTactic 1;
656 setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
657 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
659 fetchProposedTactic 1;
660 setNextTactic 1 (Rewrite_Set "norm_equation");
661 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
663 fetchProposedTactic 1;
664 setNextTactic 1 (Rewrite_Set "Test_simplify");
665 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
667 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
668 setNextTactic 1 (Subproblem ("Test",
669 ["LINEAR", "univariate", "equation", "test"]));
670 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
672 fetchProposedTactic 1;
673 setNextTactic 1 (Model_Problem );
674 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
676 fetchProposedTactic 1;
677 setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
678 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
680 fetchProposedTactic 1;
681 setNextTactic 1 (Add_Given "solveFor x");
682 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
684 fetchProposedTactic 1;
685 setNextTactic 1 (Add_Find "solutions x_i");
686 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
688 fetchProposedTactic 1;
689 setNextTactic 1 (Specify_Theory "Test");
690 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
692 fetchProposedTactic 1;
693 setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
694 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
695 "2-----------------------------------------------------------------";
697 fetchProposedTactic 1;
698 setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
699 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
701 fetchProposedTactic 1;
702 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
703 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
705 fetchProposedTactic 1;
706 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
707 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
709 fetchProposedTactic 1;
710 setNextTactic 1 (Rewrite_Set "Test_simplify");
711 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
713 fetchProposedTactic 1;
714 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
715 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
717 fetchProposedTactic 1;
718 setNextTactic 1 (Check_elementwise "Assumptions");
719 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
721 val xml = fetchProposedTactic 1;
722 setNextTactic 1 (Check_Postcond
723 ["sqroot-test", "univariate", "equation", "test"]);
724 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
726 val ((pt,_),_) = States.get_calc 1;
727 val str = pr_ctree pr_short pt;
729 val ip = States.get_pos 1 1;
730 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
731 (*exception just above means: 'ModSpec' has been returned: error anyway*)
732 if UnparseC.term f = "[x = 1]" then () else
733 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
734 (**)-------------------------------------------------------------------------------------------*)
737 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
738 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
739 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
740 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
741 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
742 ("Test", ["sqroot-test", "univariate", "equation", "test"],
743 ["Test", "squ-equ-test-subpbl1"]))];
746 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
747 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
748 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
749 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
750 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
751 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
752 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
753 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
754 (*here the solve-phase starts*)
755 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
756 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
757 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
758 (*------------------------------------*)
759 (* (*default_print_depth 13*) States.get_calc 1;
761 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
762 (*calc-head of subproblem*)
763 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
764 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
765 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
766 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
767 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
768 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
769 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
770 (*solve-phase of the subproblem*)
771 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
772 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
773 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
774 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
775 (*finish subproblem*)
776 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
778 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
780 (*this checks the test for correctness..*)
781 val ((pt,_),_) = States.get_calc 1;
782 val p = States.get_pos 1 1;
783 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
784 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
785 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
789 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
790 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
791 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
792 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
794 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
796 ["LINEAR", "univariate", "equation", "test"],
797 ["Test", "solve_linear"]))];
800 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
802 autoCalculate 1 CompleteCalc;
803 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
804 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
806 val ((pt,_),_) = States.get_calc 1;
807 val p = States.get_pos 1 1;
808 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
809 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
810 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
813 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
814 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
815 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
816 (* ERROR: error in kernel ?? *)
818 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
820 ["LINEAR", "univariate", "equation", "test"],
821 ["Test", "solve_linear"]))];
825 autoCalculate 1 CompleteCalcHead;
826 refFormula 1 (States.get_pos 1 1);
827 val ((pt,p),_) = States.get_calc 1;
829 autoCalculate 1 CompleteCalc;
830 val ((pt,p),_) = States.get_calc 1;
831 if p=([], Res) then () else
832 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
835 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
836 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
837 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
838 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
839 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
840 ("Test", ["sqroot-test", "univariate", "equation", "test"],
841 ["Test", "squ-equ-test-subpbl1"]))];
844 autoCalculate 1 CompleteCalc;
845 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
847 getTactic 1 ([1],Frm);
848 getTactic 1 ([1],Res);
849 initContext 1 Ptool.Thy_ ([1],Res);
851 (*... returns calcChangedEvent with*)
852 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
853 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
854 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
855 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
857 val ((pt,_),_) = States.get_calc 1;
858 val p = States.get_pos 1 1;
859 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
860 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
861 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
864 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
865 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
866 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
867 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
868 ("Test", ["sqroot-test", "univariate", "equation", "test"],
869 ["Test", "squ-equ-test-subpbl1"]))];
872 autoCalculate 1 CompleteCalcHead;
874 val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
876 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
877 ["Test", "squ-equ-test-subpbl1"]),
878 branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
879 ([], Met)), []) = States.get_calc 1;
880 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
881 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
884 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
885 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
886 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
889 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
891 ["LINEAR", "univariate", "equation", "test"],
892 ["Test", "solve_linear"]))];
895 autoCalculate 1 CompleteModel;
896 refFormula 1 (States.get_pos 1 1);
898 setProblem 1 ["LINEAR", "univariate", "equation", "test"];
899 val pos = States.get_pos 1 1;
900 (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
901 refFormula 1 (States.get_pos 1 1);
903 setMethod 1 ["Test", "solve_linear"];
904 (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
905 refFormula 1 (States.get_pos 1 1);
906 val ((pt,_),_) = States.get_calc 1;
907 if get_obj g_spec pt [] = (ThyC.id_empty,
908 ["LINEAR", "univariate", "equation", "test"],
909 ["Test", "solve_linear"]) then ()
910 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
912 autoCalculate 1 CompleteCalcHead;
913 refFormula 1 (States.get_pos 1 1);
914 autoCalculate 1 CompleteCalc;
918 refFormula 1 (States.get_pos 1 1);
919 val ((pt,_),_) = States.get_calc 1;
920 val p = States.get_pos 1 1;
921 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
922 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
923 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
926 "--------- setContext..Thy ------------------------------";
927 "--------- setContext..Thy ------------------------------";
928 "--------- setContext..Thy ------------------------------";
930 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
931 ("Test", ["sqroot-test", "univariate", "equation", "test"],
932 ["Test", "squ-equ-test-subpbl1"]))];
933 Iterator 1; moveActiveRoot 1;
934 autoCalculate 1 CompleteCalcHead;
935 autoCalculate 1 (Steps 1);
936 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
938 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
939 autoCalculate 1 (Steps 1);
940 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
942 "----- \<up> ^^ and vvvvv do the same -----";
943 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
944 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
946 autoCalculate 1 (Steps 1);
947 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
948 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
949 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
950 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
951 then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
953 autoCalculate 1 CompleteCalc;
954 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
955 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
957 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
958 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
961 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
962 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
963 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
965 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
966 ("Test", ["sqroot-test", "univariate", "equation", "test"],
967 ["Test", "squ-equ-test-subpbl1"]))];
968 Iterator 1; moveActiveRoot 1;
969 autoCalculate 1 CompleteToSubpbl;
970 refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
971 val ((pt,_),_) = States.get_calc 1;
972 val str = pr_ctree pr_short pt;
974 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
976 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl- 1";
978 autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
979 autoCalculate 1 CompleteToSubpbl;
980 val ((pt,_),_) = States.get_calc 1;
981 val str = pr_ctree pr_short pt;
983 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
984 val ((pt,_),_) = States.get_calc 1;
985 val p = States.get_pos 1 1;
987 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
988 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
989 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
992 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
993 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
994 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
995 "--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
996 (*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
997 ---- rat-eq + subpbl: set_found in check_tac1 ----*)
999 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
1000 ((** )"RatEq"( **)"PolyEq"(*required for "make_ratpoly_in"*),
1001 ["univariate", "equation"], ["no_met"]))];
1004 fetchProposedTactic 1;
1006 setNextTactic 1 (Model_Problem);
1007 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1009 setNextTactic 1 (Specify_Theory "RatEq");
1010 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1011 setNextTactic 1 (Specify_Problem ["rational", "univariate", "equation"]);
1012 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1013 setNextTactic 1 (Specify_Method ["RatEq", "solve_rat_equation"]);
1014 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1015 setNextTactic 1 (Apply_Method ["RatEq", "solve_rat_equation"]);
1016 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1017 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1018 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1019 setNextTactic 1 (Rewrite_Set "norm_Rational");
1020 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1021 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1022 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1023 (* __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)
1024 setNextTactic 1 (Subproblem ("PolyEq", ["normalise", "polynomial",
1025 "univariate", "equation"]));
1026 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1027 setNextTactic 1 (Model_Problem );
1028 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1029 setNextTactic 1 (Specify_Theory "PolyEq");
1030 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1031 setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1032 "univariate", "equation"]);
1033 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1034 setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1035 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1036 setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1037 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1038 setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
1039 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1040 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
1041 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1042 (* __________ for "16 + 12 * x = 0"*)
1043 setNextTactic 1 (Subproblem ("PolyEq",
1044 ["degree_1", "polynomial", "univariate", "equation"]));
1045 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1046 setNextTactic 1 (Model_Problem );
1047 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1048 setNextTactic 1 (Specify_Theory "PolyEq");
1049 (*------------- some trials in the problem-hierarchy ---------------*)
1050 setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation"]);
1051 autoCalculate 1 (Steps 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1052 setNextTactic 1 (Refine_Problem ["univariate", "equation"]);
1053 (*------------------------------------------------------------------*)
1054 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1055 setNextTactic 1 (Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1056 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1057 setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1058 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1059 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
1060 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1061 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1062 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1063 setNextTactic 1 Or_to_List;
1064 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1065 setNextTactic 1 (Check_elementwise "Assumptions");
1066 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1067 setNextTactic 1 (Check_Postcond ["degree_1", "polynomial",
1068 "univariate", "equation"]);
1069 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1070 setNextTactic 1 (Check_Postcond ["normalise", "polynomial",
1071 "univariate", "equation"]);
1072 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1073 setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
1074 val (ptp,_) = States.get_calc 1;
1075 val (Form t,_,_) = ME_Misc.pt_extract ptp;
1076 if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
1077 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1082 "--------- tryMatchProblem, tryRefineProblem ------------";
1083 "--------- tryMatchProblem, tryRefineProblem ------------";
1084 "--------- tryMatchProblem, tryRefineProblem ------------";
1085 (*{\bf\UC{Having \isac{} Refine the Problem
1086 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1087 * x \<up>2 + 4*x + 5 = 2
1088 see isac.bridge.TestSpecify#testMatchRefine*)
1091 [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
1093 ["univariate", "equation"],
1098 fetchProposedTactic 1;
1099 setNextTactic 1 (Model_Problem );
1100 (*..this tactic should be done 'tacitly', too !*)
1103 autoCalculate 1 CompleteCalcHead;
1104 checkContext 1 ([],Pbl) "pbl_equ_univ";
1105 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1108 autoCalculate 1 (Steps 1);
1110 fetchProposedTactic 1;
1111 setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");
1112 autoCalculate 1 (Steps 1);
1114 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1115 (*initContext 1 Ptool.Pbl_ ([],Pbl);*)
1116 (* this would break if a calculation would be inserted before: CALCID...
1117 and pattern matching is not available in *.java.
1118 if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
1119 then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
1121 (*initContext 1 Ptool.Met_ ([],Pbl);*)
1122 (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
1124 "--------- this match will show some incomplete items: ---------";
1126 (*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1127 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
1130 fetchProposedTactic 1;
1131 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
1133 fetchProposedTactic 1;
1134 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
1136 "--------- this is a matching model (all items correct): -------";
1137 (*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);*)
1138 "--------- this is a NOT matching model (some 'false': ---------";
1139 (*checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)
1141 "--------- find out a matching problem: ------------------------";
1142 "--------- find out a matching problem (FAILING: no new pbl) ---";
1143 refineProblem 1 ([],Pbl)(Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"]);
1145 "--------- find out a matching problem (SUCCESSFUL) ------------";
1146 refineProblem 1 ([],Pbl) (Ptool.pblID2guh @{context} ["univariate", "equation"]);
1148 "--------- tryMatch, tryRefine did not change the calculation -";
1149 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1150 setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1151 "univariate", "equation"]);
1152 autoCalculate 1 (Steps 1);
1153 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
1154 and Specify_Theory skipped in comparison to below --- \<up> -inserted *)
1155 (*------------vvv-inserted-----------------------------------------------*)
1156 fetchProposedTactic 1;
1157 (*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )
1158 setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1159 "univariate", "equation"]);
1160 autoCalculate 1 (Steps 1);
1162 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1164 fetchProposedTactic 1;
1165 setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1166 autoCalculate 1 (Steps 1);
1168 fetchProposedTactic 1;
1169 setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1171 autoCalculate 1 CompleteCalc;
1173 val ((pt,_),_) = States.get_calc 1;
1174 Test_Tool.show_pt pt;
1175 val p = States.get_pos 1 1;
1176 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1177 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1178 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1180 (*------------ \<up> -inserted-----------------------------------------------*)
1181 (*WN050904 the fetchProposedTactic's below may not have worked like that
1182 before, too, because there was no check*)
1183 fetchProposedTactic 1;
1184 setNextTactic 1 (Specify_Theory "PolyEq");
1185 autoCalculate 1 (Steps 1);
1187 fetchProposedTactic 1;
1188 setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1189 autoCalculate 1 (Steps 1);
1191 fetchProposedTactic 1;
1192 "--------- now the calc-header is ready for enter 'solving' ----";
1193 autoCalculate 1 CompleteCalc;
1195 val ((pt,_),_) = States.get_calc 1;
1197 Test_Tool.show_pt pt;
1198 val p = States.get_pos 1 1;
1199 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1200 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1201 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1203 ( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)
1205 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1206 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1207 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1209 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1210 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1211 ["Test", "squ-equ-test-subpbl1"]))];
1215 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1216 "solve (x+1=2, x)",(*the headline*)
1217 [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
1218 P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
1221 ["sqroot-test", "univariate", "equation", "test"],
1222 ["Test", "squ-equ-test-subpbl1"]));
1224 val ((Nd (PblObj {fmz = (fm, tpm),
1225 loc = (SOME scrst_ctxt, NONE),
1229 ["sqroot-test", "univariate", "equation", "test"],
1230 ["Test", "squ-equ-test-subpbl1"]),
1232 branch = TransitiveB,
1234 ostate = Incomplete,
1238 []) = States.get_calc 1;
1239 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
1240 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1241 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
1247 val ((Nd (PblObj {fmz = (fm, tpm),
1248 loc = (SOME scrst_ctxt, NONE),
1251 spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
1253 branch = TransitiveB,
1255 ostate = Incomplete,
1259 []) = States.get_calc 1;
1260 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1261 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
1263 "--------- maximum-example, UC: Modeling an example -----";
1264 "--------- maximum-example, UC: Modeling an example -----";
1265 "--------- maximum-example, UC: Modeling an example -----";
1266 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
1267 see isac.bridge.TestModel#testEditItems
1269 val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
1270 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1271 "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1272 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
1273 (* \<up> these are the elements for the root-problem (in variants)*)
1274 (*vvv these are elements required for subproblems*)
1275 "boundVariable a", "boundVariable b", "boundVariable alpha",
1276 "interval {x::real. 0 <= x & x <= 2*r}",
1277 "interval {x::real. 0 <= x & x <= 2*r}",
1278 "interval {x::real. 0 <= x & x <= pi}",
1279 "errorBound (eps=(0::real))"]
1280 (*specifying is not interesting for this example*)
1281 val spec = ("Diff_App", ["maximum_of", "function"],
1282 ["Diff_App", "max_by_calculus"]);
1283 (*the empty model with descriptions for user-guidance by Model_Problem*)
1284 val empty_model = [P_Spec.Given ["fixedValues []"],
1285 P_Spec.Find ["maximum", "valuesFor"],
1286 P_Spec.Relate ["relations []"]];
1289 "#################################################################";
1291 CalcTree @{context} [(elems, spec)];
1294 refFormula 1 (States.get_pos 1 1);
1295 (*this gives a completely empty model*)
1297 fetchProposedTactic 1;
1298 (*fill the CalcHead with Descriptions...*)
1299 setNextTactic 1 (Model_Problem );
1300 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1302 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1303 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1304 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
1305 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
1306 "Problem (Diff_App.thy, [maximum_of, function])",
1307 (*the head-form \<up> is not used for input here*)
1308 [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
1309 P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
1310 P_Spec.Relate ["relations"]],
1311 (*input (Arbfix will dissappear soon)*)
1313 References.empty (*no input to the specification*));
1315 (*the user does not know, what 'superfluous' for 'maximum b' may mean
1316 and asks what to do next*)
1317 fetchProposedTactic 1;
1318 (*the student follows the advice*)
1319 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1320 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1322 (*this input completes the model*)
1323 modifyCalcHead 1 (([],Pbl), "not used here",
1324 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1325 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1326 P_Spec.Relate ["relations [A=a*b, \
1327 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);
1329 (*specification is not interesting and should be skipped by the dialogguide;
1330 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1331 modifyCalcHead 1 (([],Pbl), "not used here",
1332 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1333 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1334 P_Spec.Relate ["relations [A=a*b, \
1335 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1336 ("Diff_App", Problem.id_empty, MethodC.id_empty));
1337 modifyCalcHead 1 (([],Pbl), "not used here",
1338 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1339 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1340 P_Spec.Relate ["relations [A=a*b, \
1341 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1342 ("Diff_App", ["maximum_of", "function"],
1344 modifyCalcHead 1 (([],Pbl), "not used here",
1345 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1346 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1347 P_Spec.Relate ["relations [A=a*b, \
1348 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1349 ("Diff_App", ["maximum_of", "function"],
1350 ["Diff_App", "max_by_calculus"]));
1351 (*this final calcHead now has STATUS 'complete' !*)
1354 (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
1355 "--------- solve_linear from pbl-hierarchy --------------";
1356 "--------- solve_linear from pbl-hierarchy --------------";
1357 "--------- solve_linear from pbl-hierarchy --------------";
1359 val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
1360 CalcTree @{context} [(fmz, sp)];
1361 Iterator 1; moveActiveRoot 1;
1362 refFormula 1 (States.get_pos 1 1);
1363 modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
1364 [P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
1365 P_Spec.Find ["solutions L"]],
1367 ("Test", ["LINEAR", "univariate", "equation", "test"],
1368 ["Test", "solve_linear"]));
1369 autoCalculate 1 CompleteCalc;
1370 refFormula 1 (States.get_pos 1 1);
1371 val ((pt,_),_) = States.get_calc 1;
1372 val p = States.get_pos 1 1;
1373 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1374 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1375 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
1378 "--------- solve_linear as in an algebra system (CAS)----";
1379 "--------- solve_linear as in an algebra system (CAS)----";
1380 "--------- solve_linear as in an algebra system (CAS)----";
1381 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
1383 val (fmz, sp) = ([], ("", [], []));
1384 CalcTree @{context} [(fmz, sp)];
1385 Iterator 1; moveActiveRoot 1;
1386 modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
1387 autoCalculate 1 CompleteCalc;
1388 refFormula 1 (States.get_pos 1 1);
1389 val ((pt,_),_) = States.get_calc 1;
1390 val p = States.get_pos 1 1;
1391 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1392 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1393 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
1397 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1398 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1399 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1400 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1401 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1402 ["Test", "squ-equ-test-subpbl1"]))];
1405 autoCalculate 1 CompleteCalc;
1406 val ((pt,_),_) = States.get_calc 1;
1407 Test_Tool.show_pt pt;
1409 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1410 interSteps 1 ([2],Res);
1411 val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1412 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1413 getFormulaeFromTo 1 unc gen 1 false;
1415 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1416 interSteps 1 ([3,2],Res);
1417 val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1418 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1419 getFormulaeFromTo 1 unc gen 1 false;
1421 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1422 interSteps 1 ([3],Res) (*no new steps in subproblems*);
1423 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1424 getFormulaeFromTo 1 unc gen 1 false;
1426 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1427 interSteps 1 ([],Res) (*no new steps in subproblems*);
1428 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1429 getFormulaeFromTo 1 unc gen 1 false;
1432 "--------- getTactic, fetchApplicableTactics ------------";
1433 "--------- getTactic, fetchApplicableTactics ------------";
1434 "--------- getTactic, fetchApplicableTactics ------------";
1435 (* compare test/../script.sml
1436 "----------- fun from_prog ---------------------------------------";
1438 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1439 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1440 ["Test", "squ-equ-test-subpbl1"]))];
1441 Iterator 1; moveActiveRoot 1;
1442 autoCalculate 1 CompleteCalc;
1443 val ((pt,_),_) = States.get_calc 1;
1444 Test_Tool.show_pt pt;
1446 (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1447 WN120210 not impl. in FE*)
1448 getTactic 1 ([],Pbl);
1449 getTactic 1 ([1],Res);
1450 getTactic 1 ([3],Pbl);
1451 getTactic 1 ([3,1],Frm);
1452 getTactic 1 ([3],Res);
1453 getTactic 1 ([],Res);
1455 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1456 fetchApplicableTactics 1 99999 ([],Pbl);
1457 fetchApplicableTactics 1 99999 ([1],Res);
1458 fetchApplicableTactics 1 99999 ([3],Pbl);
1459 fetchApplicableTactics 1 99999 ([3,1],Res);
1460 fetchApplicableTactics 1 99999 ([3],Res);
1461 fetchApplicableTactics 1 99999 ([],Res);
1464 (*SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\* )
1465 "--------- getAssumptions, getAccumulatedAsms -----------";
1466 "--------- getAssumptions, getAccumulatedAsms -----------";
1467 "--------- getAssumptions, getAccumulatedAsms -----------";
1470 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
1471 "solveFor x", "solutions L"],
1472 ("RatEq",["univariate", "equation"],["no_met"]))];
1473 Iterator 1; moveActiveRoot 1;
1474 autoCalculate 1 CompleteCalc;
1475 val ((pt,_),_) = States.get_calc 1;
1476 val p = States.get_pos 1 1;
1477 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1478 (*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
1479 if map UnparseC.term asms =
1480 ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
1481 " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0",
1482 "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
1483 "lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2",
1484 "9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"]
1485 andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()
1486 else error "TODO compare 2002-- 2011"; (*...data during test --- x / (x \<up> 2 - 6 * x + 9) - 1...*)
1487 ============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)
1489 if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
1490 andalso map UnparseC.term asms = []
1491 then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1493 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1494 getAssumptions 1 ([3], Res);
1495 getAssumptions 1 ([5], Res);
1496 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1497 WN0502 still without positions*)
1498 getAccumulatedAsms 1 ([3], Res);
1499 getAccumulatedAsms 1 ([5], Res);
1501 ( *SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//*)
1504 "--------- arbitrary combinations of steps --------------";
1505 "--------- arbitrary combinations of steps --------------";
1506 "--------- arbitrary combinations of steps --------------";
1507 CalcTree @{context} (*start of calculation, return No.1*)
1508 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1510 ["LINEAR", "univariate", "equation", "test"],
1511 ["Test", "solve_linear"]))];
1512 Iterator 1; moveActiveRoot 1;
1514 fetchProposedTactic 1;
1515 (*ERROR States.get_calc 1 not existent*)
1516 setNextTactic 1 (Model_Problem );
1517 autoCalculate 1 (Steps 1);
1518 fetchProposedTactic 1;
1519 fetchProposedTactic 1;
1521 setNextTactic 1 (Add_Find "solutions L");
1522 setNextTactic 1 (Add_Find "solutions L");
1524 autoCalculate 1 (Steps 1);
1525 autoCalculate 1 (Steps 1);
1527 setNextTactic 1 (Specify_Theory "Test");
1528 fetchProposedTactic 1;
1529 autoCalculate 1 (Steps 1);
1531 autoCalculate 1 (Steps 1);
1532 autoCalculate 1 (Steps 1);
1533 autoCalculate 1 (Steps 1);
1534 autoCalculate 1 (Steps 1);
1535 (*------------------------- end calc-head*)
1537 fetchProposedTactic 1;
1538 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1539 autoCalculate 1 (Steps 1);
1541 setNextTactic 1 (Rewrite_Set "Test_simplify");
1542 fetchProposedTactic 1;
1543 autoCalculate 1 (Steps 1);
1545 autoCalculate 1 CompleteCalc;
1546 val ((pt,_),_) = States.get_calc 1;
1547 val p = States.get_pos 1 1;
1548 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1549 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1550 error "FE-interface.sml: diff.behav. in combinations of steps";
1553 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1554 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1555 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1557 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1558 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1559 ["Test", "squ-equ-test-subpbl1"]))];
1562 autoCalculate 1 CompleteCalcHead;
1563 autoCalculate 1 (Steps 1);
1564 autoCalculate 1 (Steps 1);
1565 appendFormula 1 "- 1 + x = 0" (*|> Future.join*);
1566 (*... returns calcChangedEvent with*)
1567 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1568 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1570 val ((pt,_),_) = States.get_calc 1;
1571 val p = States.get_pos 1 1;
1572 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1573 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1574 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1577 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1578 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1579 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1580 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1581 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1582 ["Test", "squ-equ-test-subpbl1"]))];
1585 autoCalculate 1 CompleteCalcHead;
1586 autoCalculate 1 (Steps 1);
1587 autoCalculate 1 (Steps 1);
1588 appendFormula 1 "x - 1 = 0" (*|> Future.join*);
1589 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1590 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1593 val ((pt,_),_) = States.get_calc 1;
1594 val p = States.get_pos 1 1;
1595 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1596 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1597 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1600 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1601 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1602 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1603 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1604 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1605 ["Test", "squ-equ-test-subpbl1"]))];
1608 autoCalculate 1 CompleteCalcHead;
1609 autoCalculate 1 (Steps 1);
1610 autoCalculate 1 (Steps 1);
1611 appendFormula 1 "x = 1" (*|> Future.join*);
1612 (*... returns calcChangedEvent with*)
1613 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1614 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1617 val ((pt,_),_) = States.get_calc 1;
1618 val p = States.get_pos 1 1;
1619 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1620 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1621 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1624 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1625 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1626 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1627 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1628 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1629 ["Test", "squ-equ-test-subpbl1"]))];
1632 autoCalculate 1 CompleteCalcHead;
1633 autoCalculate 1 (Steps 1);
1634 autoCalculate 1 (Steps 1);
1635 appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
1636 (*... returns <ERROR> no derivation found </ERROR>*)
1638 val ((pt,_),_) = States.get_calc 1;
1639 val p = States.get_pos 1 1;
1640 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1641 if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
1642 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1645 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1646 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1647 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1648 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1649 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1650 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1651 ["Test", "squ-equ-test-subpbl1"]))];
1654 autoCalculate 1 CompleteCalc;
1655 moveActiveFormula 1 ([2],Res);
1656 replaceFormula 1 "- 1 + x = 0" (*i.e. repeats input*);
1657 (*... returns <ERROR> formula not changed </ERROR>*)
1659 val ((pt,_),_) = States.get_calc 1;
1660 val p = States.get_pos 1 1;
1661 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1662 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1663 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1664 if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1665 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1666 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1667 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1669 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1670 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1671 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1672 ["Test", "squ-equ-test-subpbl1"]))];
1673 Iterator 2; (*! ! ! 1 CalcTree @{context} inbetween States.reset (); *)
1675 autoCalculate 2 CompleteCalc;
1676 moveActiveFormula 2 ([2],Res);
1677 replaceFormula 2 "- 1 + x = 0" (*i.e. repeats input*);
1678 (*... returns <ERROR> formula not changed </ERROR>*)
1680 val ((pt,_),_) = States.get_calc 2;
1681 val p = States.get_pos 2 1;
1682 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1683 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1684 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1685 if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1686 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1687 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1688 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1691 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1692 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1693 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1694 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1695 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1696 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1697 ["Test", "squ-equ-test-subpbl1"]))];
1700 autoCalculate 1 CompleteCalc;
1701 moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1702 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1703 (*... returns calcChangedEvent with*)
1704 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1705 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1707 val ((pt,_),_) = States.get_calc 1;
1708 Test_Tool.show_pt pt;
1709 val p = States.get_pos 1 1;
1710 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1711 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1712 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1713 (* for getting the list in whole length ...
1714 (*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1716 if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1717 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1718 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1719 ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
1720 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1723 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1724 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1725 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1726 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1727 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1728 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1729 ["Test", "squ-equ-test-subpbl1"]))];
1732 autoCalculate 1 CompleteCalc;
1733 moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1734 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1735 (*... returns calcChangedEvent with ...*)
1736 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1737 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1740 val ((pt,_),_) = States.get_calc 1;
1741 Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
1742 val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
1743 if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1744 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1745 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1746 ([3,2],Res)] then () else
1747 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1749 val p = States.get_pos 1 1;
1750 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1751 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1752 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1756 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1757 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1758 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1759 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1760 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1761 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1762 ["Test", "squ-equ-test-subpbl1"]))];
1765 autoCalculate 1 CompleteCalc;
1766 moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1767 replaceFormula 1 "x - 4711 = 0";
1768 (*... returns <ERROR> no derivation found </ERROR>*)
1770 val ((pt,_),_) = States.get_calc 1;
1771 Test_Tool.show_pt pt;
1772 val p = States.get_pos 1 1;
1773 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1774 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1775 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1778 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1779 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1780 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1782 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1783 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1786 autoCalculate 1 CompleteCalcHead;
1787 autoCalculate 1 (Steps 1);
1788 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1789 appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1790 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1791 would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1792 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1793 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1794 val ((pt,pos), _) = States.get_calc 1;
1795 val p = States.get_pos 1 1;
1796 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1798 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1799 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1800 ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
1801 | _ => error "embed fun fill_form changed 1"
1802 else error "embed fun fill_form changed 2";
1804 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1805 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1806 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
1807 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1808 val ((pt,pos),_) = States.get_calc 1;
1809 val p = States.get_pos 1 1;
1811 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1812 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1813 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1815 else error "embed fun fill_form changed 2";
1817 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1818 and the last has no gaps, then the number of fill-patterns would suffice
1819 for the DialogGuide to select appropriately. *)
1820 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1821 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1822 val ((pt,pos),_) = States.get_calc 1;
1823 val p = States.get_pos 1 1;
1824 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1825 if p = ([1], Res) andalso existpt [2] pt andalso
1826 UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
1827 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
1828 then () else error "embed fun fill_form changed 3";
1830 inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
1831 val ((pt, _),_) = States.get_calc 1;
1832 val p = States.get_pos 1 1;
1833 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1834 if p = ([2], Res) andalso
1835 UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
1836 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
1837 then () else error "inputFillFormula changed 11";
1839 autoCalculate 1 CompleteCalc;
1841 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1842 val ((pt, _),_) = States.get_calc 1;
1843 val p = States.get_pos 1 1;
1844 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1845 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
1846 then () else error "inputFillFormula changed 12";
1847 Test_Tool.show_pt pt;
1849 (([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),
1850 (([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),
1851 (([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),
1852 (([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)), (*<<<<<<<=====*)
1853 (([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1854 (([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1855 (([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),
1856 (([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)
1857 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1861 (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
1862 "--------- UC errpat add-fraction, fillpat by input --------------";
1863 "--------- UC errpat add-fraction, fillpat by input --------------";
1864 "--------- UC errpat add-fraction, fillpat by input --------------";
1865 (*cp from BridgeLog Java <=> SML*)
1866 CalcTree @{context} [([], References.empty)];
1869 moveActiveFormula 1 ([],Pbl);
1870 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1871 autoCalculate 1 CompleteCalcHead;
1872 autoCalculate 1 (Steps 1);
1873 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
1874 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1875 --- but in BridgeLog Java <=> SML:
1876 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1878 -----------------------------------------------------------------------------------------------*)
1881 "--------- UC errpat, fillpat step to Rewrite --------------------";
1882 "--------- UC errpat, fillpat step to Rewrite --------------------";
1883 "--------- UC errpat, fillpat step to Rewrite --------------------";
1886 [(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1887 "differentiateFor x", "derivative f_f'"],
1888 ("Isac_Knowledge", ["derivative_of", "function"],
1889 ["diff", "differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1892 autoCalculate 1 CompleteCalc;
1893 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1897 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1898 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1899 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1901 [(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1902 "differentiateFor x", "derivative f_f'"],
1903 ("Isac_Knowledge", ["derivative_of", "function"],
1904 ["diff", "after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1907 autoCalculate 1 CompleteCalcHead;
1908 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1909 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1912 <CALCID> 1 </CALCID>
1913 <TACTICERRORPATTERNS>
1915 <STRING> chain-rule-diff-both </STRING>
1916 <STRING> cancel </STRING>
1918 <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1919 <RULESET> norm_diff </RULESET>
1934 </REWRITESETINSTTACTIC>
1935 </TACTICERRORPATTERNS>
1939 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1940 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1941 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1942 (* then --- UC errpat, fillpat by input ---*)
1944 autoCalculate 1 CompleteCalc;
1945 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1946 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1953 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1954 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1955 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1963 section \<open>history of tests\<close>
1965 Systematic regression tests have been introduced to isac development in 2003.
1966 Sanity of the regression tests suffers from updates following Isabelle development,
1967 which mostly exceeded the resources available in isac's development.
1969 The survey below shall support to efficiently use the tests for isac
1970 on different Isabelle versions. Conclusion in most cases will be:
1972 !!! Use most recent tests or go back to the old notebook
1973 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1977 subsection \<open>isac on Isabelle2017\<close>
1978 subsubsection \<open>Summary of development\<close>
1980 * Add further signatures, separate structures and cleanup respective files.
1981 * Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
1982 * Clean theory dependencies.
1983 * Start preparing shift from isac-java to Isabelle/jEdit.
1985 subsubsection \<open>State of tests: unchanged\<close>
1986 subsubsection \<open>Changesets of begin and end\<close>
1988 last changeset with Test_Isac 925fef0f4c81
1989 first changeset with Test_Isac bbb414976dfe
1992 subsection \<open>isac on Isabelle2015\<close>
1993 subsubsection \<open>Summary of development\<close>
1995 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
1996 This complicates Test_Isac, see "Prepare running tests" above.
1997 * Remove TTY interface.
1998 * Re-activate insertion sort.
2000 subsubsection \<open>State of tests: unchanged\<close>
2001 subsubsection \<open>Changesets of begin and end\<close>
2003 last changeset with Test_Isac 2f1b2854927a
2004 first changeset with Test_Isac ???
2007 subsection \<open>isac on Isabelle2014\<close>
2008 subsubsection \<open>Summary of development\<close>
2010 migration from "isabelle tty" --> libisabelle
2013 subsection \<open>isac on Isabelle2013-2\<close>
2014 subsubsection \<open>Summary of development\<close>
2016 reactivated context_thy
2018 subsubsection \<open>State of tests\<close>
2022 subsubsection \<open>Changesets of begin and end\<close>
2026 : isac on Isablle2013-2
2028 Changeset: 55318 (03826ceb24da) merged
2029 User: Walther Neuper <neuper@ist.tugraz.at>
2030 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
2033 subsection \<open>isac on Isabelle2013-1\<close>
2034 subsubsection \<open>Summary of development\<close>
2036 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
2037 no significant development steps for ISAC.
2039 subsubsection \<open>State of tests\<close>
2041 See points in subsection "isac on Isabelle2011", "State of tests".
2043 subsubsection \<open>Changesets of begin and end\<close>
2045 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
2046 User: Walther Neuper <neuper@ist.tugraz.at>
2047 Date: 2013-12-03 18:13:31 +0100 (8 days)
2049 : isac on Isablle2013-1
2051 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
2052 User: Walther Neuper <neuper@ist.tugraz.at>
2053 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
2057 subsection \<open>isac on Isabelle2013\<close>
2058 subsubsection \<open>Summary of development\<close>
2060 # Oct.13: replaced "axioms" by "axiomatization"
2061 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
2062 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
2063 simplification of multivariate rationals (without improving the rulesets involved).
2065 subsubsection \<open>Run tests\<close>
2067 Is standard now; this subsection will be discontinued under Isabelle2013-1
2069 subsubsection \<open>State of tests\<close>
2071 See points in subsection "isac on Isabelle2011", "State of tests".
2072 # re-activated listC.sml
2074 subsubsection \<open>Changesets of begin and end\<close>
2076 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
2077 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
2078 Date: Tue Nov 19 22:23:30 2013 +0000
2080 : isac on Isablle2013
2082 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
2083 User: Walther Neuper <neuper@ist.tugraz.at>
2084 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
2087 subsection \<open>isac on Isabelle2012\<close>
2088 subsubsection \<open>Summary of development\<close>
2090 isac on Isabelle2012 is considered just a transitional stage
2091 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
2092 For considerations on the transition see
2093 $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
2095 subsubsection \<open>Run tests\<close>
2097 $ cd /usr/local/isabisac12/
2098 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
2099 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
2101 subsubsection \<open>State of tests\<close>
2103 At least the tests from isac on Isabelle2011 run again.
2104 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
2105 in parallel with evaluation.
2107 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
2108 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
2109 (i.e. on the old notebook from 2002).
2111 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
2112 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
2113 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
2114 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
2115 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
2117 Some tests have been re-activated (e.g. error patterns, fill patterns).
2119 subsubsection \<open>Changesets of begin and end\<close>
2121 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
2122 User: Walther Neuper <neuper@ist.tugraz.at>
2123 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
2125 : isac on Isablle2012
2127 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
2128 User: Walther Neuper <neuper@ist.tugraz.at>
2129 Date: 2012-09-24 18:35:13 +0200 (8 months)
2130 ------------------------------------------------------------------------------
2131 Changeset: 48756 (7443906996a8) merged
2132 User: Walther Neuper <neuper@ist.tugraz.at>
2133 Date: 2012-09-24 18:15:49 +0200 (8 months)
2136 subsection \<open>isac on Isabelle2011\<close>
2137 subsubsection \<open>Summary of development\<close>
2139 isac's mathematics engine has been extended by two developments:
2140 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
2141 (2) Z_Transform was introduced by Jan Rocnik, which revealed
2142 further errors introduced by (1).
2143 (3) "error patterns" were introduced by Gabriella Daroczy
2144 Regressions tests have been added for all of these.
2146 subsubsection \<open>Run tests\<close>
2148 $ cd /usr/local/isabisac11/
2149 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
2150 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
2152 subsubsection \<open>State of tests\<close>
2154 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
2155 and sometimes give reasons for failing tests.
2156 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
2157 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
2159 The most signification tests (in particular Frontend/interface.sml) run,
2160 however, many "error in kernel" are not caught by an exception.
2161 ------------------------------------------------------------------------------
2162 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
2163 ------------------------------------------------------------------------------
2164 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
2165 User: Walther Neuper <neuper@ist.tugraz.at>
2166 Date: 2012-08-06 10:38:11 +0200 (11 months)
2169 The list below records TODOs while producing an ISAC kernel for
2170 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
2171 (so to be resumed with Isabelle2013-1):
2172 ############## WNxxxxxx.TODO can be found in sources ##############
2173 --------------------------------------------------------------------------------
2174 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
2175 --------------------------------------------------------------------------------
2176 WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
2177 this special case (see) --- why not nxt = Model_Problem here ? ---
2178 --------------------------------------------------------------------------------
2179 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
2181 # simplify_* , *_simp_*
2183 # calc_* , calculate_* ... require iteration over all rls ...
2184 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
2185 --------------------------------------------------------------------------------
2186 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
2187 --------------------------------------------------------------------------------
2188 WN120314 changeset a393bb9f5e9f drops root equations.
2189 see test/Tools/isac/Knowledge/rootrateq.sml
2190 --------------------------------------------------------------------------------
2191 WN120317.TODO changeset 977788dfed26 dropped rateq:
2192 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
2193 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
2194 investigation Check_elementwise stopped due to too much effort finding out,
2195 why Check_elementwise worked in 2002 in spite of the error.
2196 --------------------------------------------------------------------------------
2197 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
2198 --------------------------------------------------------------------------------
2199 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
2200 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
2201 --------------------------------------------------------------------------------
2202 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
2203 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
2204 --------------------------------------------------------------------------------
2205 WN120320.TODO check-improve rlsthmsNOTisac:
2206 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
2207 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
2208 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
2209 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
2210 --------------------------------------------------------------------------------
2211 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
2212 --------------------------------------------------------------------------------
2213 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
2214 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
2215 --------------------------------------------------------------------------------
2216 WN120321.TODO rearrange theories:
2220 ///Input_Descript.thy --> ProgLang
2221 Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
2222 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
2223 Interpret.thy are generated (simplifies xml structure for theories)
2226 ListC.thy <--- first_Proglang_thy
2227 --------------------------------------------------------------------------------
2228 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
2229 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
2230 broken during work on thy-hierarchy
2231 --------------------------------------------------------------------------------
2232 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
2233 test --- the_hier (get_thes ()) (collect_thydata ())---
2234 --------------------------------------------------------------------------------
2235 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
2236 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
2237 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
2238 --------------------------------------------------------------------------------
2239 WN120411 scanning html representation of newly generated knowledge:
2241 ** Theorems: only "Proof of the theorem" (correct!)
2242 and "(c) isac-team (math-autor)"
2243 ** Rulesets: only "Identifier:///"
2244 and "(c) isac-team (math-autor)"
2245 ** IsacKnowledge: link to dependency graph (which needs to be created first)
2246 ** IsacScripts --> ProgramLanguage
2247 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
2252 ** Z-Transform is missing !!!
2253 ** type-constraints !!!
2254 --------------------------------------------------------------------------------
2255 WN120417: merging xmldata revealed:
2256 ..............NEWLY generated:........................................
2258 <GUH> thy_isab_Fun-thm-o_apply </GUH>
2260 <STRING> Isabelle </STRING>
2261 <STRING> Fun </STRING>
2262 <STRING> Theorems </STRING>
2263 <STRING> o_apply </STRING>
2266 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
2269 <TEXT> Proof of the theorem </TEXT>
2270 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
2273 <EXPLANATIONS> </EXPLANATIONS>
2275 <STRING> Isabelle team, TU Munich </STRING>
2280 ..............OLD FORMAT:.............................................
2282 <GUH> thy_isab_Fun-thm-o_apply </GUH>
2284 <STRING> Isabelle </STRING>
2285 <STRING> Fun </STRING>
2286 <STRING> Theorems </STRING>
2287 <STRING> o_apply </STRING>
2292 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
2297 <TEXT> Proof of the theorem </TEXT>
2298 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
2301 <EXPLANATIONS> </EXPLANATIONS>
2303 <STRING> Isabelle team, TU Munich </STRING>
2308 --------------------------------------------------------------------------------
2310 subsubsection \<open>Changesets of begin and end\<close>
2312 isac development was done between these changesets:
2313 ------------------------------------------------------------------------------
2314 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
2315 User: Walther Neuper <neuper@ist.tugraz.at>
2316 Date: 2012-09-24 16:39:30 +0200 (8 months)
2318 : isac on Isablle2011
2320 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
2321 Branch: decompose-isar
2322 User: Walther Neuper <neuper@ist.tugraz.at>
2323 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
2324 ------------------------------------------------------------------------------
2327 subsection \<open>isac on Isabelle2009-2\<close>
2328 subsubsection \<open>Summary of development\<close>
2330 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
2331 The update was painful (bridging 7 years of Isabelle development) and cut short
2332 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
2333 going on to Isabelle2011 although most of the tests did not run.
2335 subsubsection \<open>Run tests\<close>
2337 WN131021 this is broken by installation of Isabelle2011/12/13,
2338 because all these write their binaries to ~/.isabelle/heaps/..
2340 $ cd /usr/local/isabisac09-2/
2341 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
2342 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
2343 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
2345 subsubsection \<open>State of tests\<close>
2347 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
2349 subsubsection \<open>Changesets of begin and end\<close>
2351 isac development was done between these changesets:
2352 ------------------------------------------------------------------------------
2353 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
2354 Branch: decompose-isar
2355 User: Marco Steger <m.steger@student.tugraz.at>
2356 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
2358 : isac on Isablle2009-2
2360 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
2361 Branch: isac-from-Isabelle2009-2
2362 User: Walther Neuper <neuper@ist.tugraz.at>
2363 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
2364 ------------------------------------------------------------------------------
2367 subsection \<open>isac on Isabelle2002\<close>
2368 subsubsection \<open>Summary of development\<close>
2370 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
2371 of isac's mathematics engine has been implemented.
2373 subsubsection \<open>Run tests\<close>
2374 subsubsection \<open>State of tests\<close>
2376 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
2377 recent Linux versions)
2379 subsubsection \<open>Changesets of begin and end\<close>
2381 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
2382 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
2386 (*========== inhibit exn 130719 Isabelle2013 ===================================
2387 ============ inhibit exn 130719 Isabelle2013 =================================*)
2389 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2390 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)