TermC: error caused by broken test shows: get_theory "Pure" ...
... causes msg: undefined entry for theory "Isac.Pure"
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 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
8 ~~/test/Tools/isac/ADDTESTS
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
10 -------------------------------------------------------------------------------
12 Prepare running tests: see below
14 $ cd /usr/local/isabisac/
15 $ export ISABELLE_VERSION=2015 # for libisabelle
16 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
19 section \<open>Prepare running tests\<close>
21 Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
22 This policy conflicts with those tests, which go into functions to details
23 not declared in the signatures.
25 In order to maintain these tests without changes, this has to be done before running tests:
26 (1) Extend signatures for tests by
27 ~~$ ./xcoding-to-test.sh
28 ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
29 Running Test_Isac.thy opens all structures, see code after "begin" below.
30 (2) Clean signatures for coding
31 ~~$ ./xtest-to-coding.sh
32 ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
34 ********************* don't forget (2) BEFORE pushing to repository *********************
36 The above bash files accomplish query replace in src/Tools/isac:
37 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
38 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
39 ^^^ in signature outcommented, ^^^ NOT outcommented,
40 this is status for coding this is status for tests
43 section \<open>code for copy & paste\<close>
45 "~~~~~ fun , args:"; val () = ();
46 "~~~~~ and , args:"; val () = ();
48 "~~~~~ to return val:"; val () = ();
51 section \<open>Run the tests\<close>
53 * say "OK" to the popup asking for theories to be loaded
54 * watch the <Theories> window for errors in the "imports" below
57 theory Test_Isac imports Build_Thydata
58 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
59 "ADDTESTS/accumulate-val/Thy_All"
61 "ADDTESTS/test-depend/Build_Test"
64 "ADDTESTS/course/phst11/T1_Basics"
65 "ADDTESTS/course/phst11/T2_Rewriting"
66 "ADDTESTS/course/phst11/T3_MathEngine"
67 "ADDTESTS/file-depend/BuildC_Test"
68 "ADDTESTS/session-get_theory/Foo"
69 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
70 ADDTESTS/------------------------------------------- see end of tests *)
71 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
72 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
73 "~~/test/Pure/Isar/Test_Parse_Term"
74 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
75 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
76 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
80 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
81 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
82 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
83 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
84 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
85 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
90 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
91 (* these vvv test, if funs are intermediately opened in structure
92 in case of errors here consider ~~/./xtest-to-coding.sh *)
94 open Math_Engine; CalcTreeTEST;
96 open Inform; cas_input;
97 open Rtools; trtas2str;
98 open Chead; pt_extract;
99 open Generate; (* NONE *)
100 open Ctree; append_problem;
101 open Specify; show_ptyps;
102 open Applicable; mk_set;
103 open Solve; (* NONE *)
105 open Stool; transfer_asms_from_to;
107 open Model; (* NONE *)
108 open LTool; rule2stac;
109 open Rewrite; mk_thm;
112 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
116 "~~~~~ fun xxx, args:"; val () = ();
122 KEStore_Elems.set_ref_thy @{theory};
123 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
126 (*---------------------- check test file by testfile -------------------------------------------
127 ---------------------- check test file by testfile -------------------------------------------*)
128 section {* trials with Isabelle's functions *}
129 ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
130 ML_file "~~/test/Pure/General/alist.ML"
131 ML_file "~~/test/Pure/General/basics.ML"
132 ML_file "~~/test/Pure/General/scan.ML"
133 ML_file "~~/test/Pure/PIDE/xml.ML"
134 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
136 section {* test ML Code of isac *}
137 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
138 ML_file "library.sml"
139 ML_file "calcelems.sml"
140 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
141 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
142 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
143 ML_file "ProgLang/termC.sml"
144 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
145 ML_file "ProgLang/rewrite.sml"
146 ML_file "ProgLang/listC.sml"
147 ML_file "ProgLang/scrtools.sml"
148 ML_file "ProgLang/tools.sml"
149 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
150 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
151 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
152 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
153 ML_file "Minisubpbl/000-comments.sml"
154 ML_file "Minisubpbl/100-init-rootpbl.sml"
155 ML_file "Minisubpbl/150-add-given.sml"
156 ML_file "Minisubpbl/200-start-method.sml"
157 ML_file "Minisubpbl/300-init-subpbl.sml"
158 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
159 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
160 ML_file "Minisubpbl/500-met-sub-to-root.sml"
161 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
162 ML_file "Minisubpbl/600-postcond.sml"
163 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
164 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
165 ML_file "Interpret/mstools.sml"
166 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
167 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
168 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
169 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
170 ML_file "Interpret/generate.sml"
171 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
172 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
173 ML_file "Interpret/calchead.sml"
174 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
175 ML_file "Interpret/rewtools.sml"
176 ML_file "Interpret/script.sml"
177 ML_file "Interpret/solve.sml"
178 ML_file "Interpret/inform.sml"
179 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
180 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
181 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
183 "----------- fun autoCalculate -----------------------------------";
185 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
186 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
187 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
190 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
191 modeling is skipped FIXME
192 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
193 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
194 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
196 fetchProposedTactic 1;
197 setNextTactic 1 (Add_Given "solveFor x");
198 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
200 fetchProposedTactic 1;
201 setNextTactic 1 (Add_Find "solutions L");
202 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
204 fetchProposedTactic 1;
205 setNextTactic 1 (Specify_Theory "Test");
206 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
207 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
208 autoCalculate 1 (Step 1);
210 autoCalculate 1 (Step 1);
212 autoCalculate 1 (Step 1);
214 autoCalculate 1 (Step 1);
217 autoCalculate 1 (Step 1);
218 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
220 term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)";
223 autoCalculate 1 (Step 1);
224 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
229 autoCalculate 1 (Step 1);
230 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
235 autoCalculate 1 (Step 1);
236 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
241 autoCalculate 1 (Step 1);
242 val (ptp as (_, p), _) = get_calc 1;
243 val (Form t,_,_) = pt_extract ptp;
247 term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)"
249 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
250 else error "mathengine.sml -- fun autoCalculate -- end";
254 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
255 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
256 ML_file "xmlsrc/mathml.sml" (*part.*)
257 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
258 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
259 ML_file "xmlsrc/thy-hierarchy.sml"
260 ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
261 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
262 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
263 ML_file "Frontend/messages.sml"
264 ML_file "Frontend/states.sml"
265 ML_file "Frontend/interface.sml"
266 ML_file "Frontend/use-cases.sml"
267 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
268 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
269 ML_file "print_exn_G.sml"
270 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
271 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
272 ML_file "Knowledge/delete.sml"
273 ML_file "Knowledge/descript.sml"
274 ML_file "Knowledge/atools.sml"
275 ML_file "Knowledge/simplify.sml"
276 ML_file "Knowledge/poly.sml"
277 ML_file "Knowledge/gcd_poly_ml.sml"
278 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
279 ML_file "Knowledge/rational.sml"
280 ML_file "Knowledge/equation.sml"
281 ML_file "Knowledge/root.sml"
282 ML_file "Knowledge/lineq.sml"
283 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
284 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
285 ML_file "Knowledge/rootrat.sml"
286 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
287 ML_file "Knowledge/partial_fractions.sml"
288 ML_file "Knowledge/polyeq.sml"
289 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
290 ML_file "Knowledge/calculus.sml"
291 ML_file "Knowledge/trig.sml"
292 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
293 ML_file "Knowledge/diff.sml"
294 ML_file "Knowledge/integrate.sml"
298 "----------- simplify by ruleset reducing make_ratpoly_in";
299 val thy = @{theory "Isac"};
301 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
303 "----- stepwise from the rulesets in simplify_Integral and below-----";
304 val rls = norm_Rational_noadd_fractions;
305 case rewrite_set_inst_ thy true subs rls t of
306 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
310 val rls = order_add_mult_in;
311 val SOME (t,[]) = rewrite_set_ thy true rls t;
312 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
313 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
316 val rls = discard_parentheses;
317 val SOME (t,[]) = rewrite_set_ thy true rls t;
318 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
319 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
323 (append_rls "separate_bdv" collect_bdv
324 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
325 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
326 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
327 (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
328 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
329 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
330 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
331 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
333 (*show_types := true; --- do we need type-constraint in thms? *)
334 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
335 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
336 @{thm separate_1_bdv}; (*::?'a*)
337 val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
338 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
339 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
341 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
342 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
343 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
346 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
347 val rls = simplify_Integral;
348 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
349 (* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
350 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
351 else error "integrate.sml, simplify_Integral #99";
353 "........... 2nd integral ........................................";
354 "........... 2nd integral ........................................";
355 "........... 2nd integral ........................................";
357 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
358 val rls = simplify_Integral;
359 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
361 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
362 then () else raise error "integrate.sml, simplify_Integral #198";
364 val rls = integration_rules;
365 val SOME (t,[]) = rewrite_set_ thy true rls t;
368 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
369 then () else error "integrate.sml, simplify_Integral #199";
372 "----------- integrate by ruleset -----------------------";*} ML {*
375 ML_file "Knowledge/eqsystem.sml"
376 ML_file "Knowledge/test.sml"
377 ML_file "Knowledge/polyminus.sml"
378 ML_file "Knowledge/vect.sml"
379 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
380 ML_file "Knowledge/biegelinie-1.sml"
384 (* tests on biegelinie
385 author: Walther Neuper 050826
386 (c) due to copyright terms
389 trace_rewrite := false;
390 "-----------------------------------------------------------------";
391 "table of contents -----------------------------------------------";
392 "-----------------------------------------------------------------";
393 "----------- the rules -------------------------------------------";
394 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
395 "----------- simplify_leaf for this script -----------------------";
396 "----------- Bsp 7.27 me -----------------------------------------";
397 "----------- Bsp 7.27 autoCalculate ------------------------------";
398 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
399 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
400 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
401 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
402 "----------- investigate normalforms in biegelinien --------------";
403 "-----------------------------------------------------------------";
404 "-----------------------------------------------------------------";
405 "-----------------------------------------------------------------";
407 val thy = @{theory "Biegelinie"};
408 val ctxt = thy2ctxt' "Biegelinie";
409 fun str2term str = (Thm.term_of o the o (parse thy)) str;
410 fun term2s t = term_to_string'' "Biegelinie" t;
412 fst (the (rewrite_ thy tless_true e_rls true thm str));
415 "----------- the rules -------------------------------------------";
416 "----------- the rules -------------------------------------------";
417 "----------- the rules -------------------------------------------";
418 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
419 if term2s t = "Q' x = - q_0" then ()
420 else error "/biegelinie.sml: Belastung_Querkraft";
422 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
423 if term2s t = "M_b' x = - q_0 * x + c" then ()
424 else error "/biegelinie.sml: Querkraft_Moment";
426 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
428 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
429 else error "biegelinie.sml: Moment_Neigung";
432 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
433 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
434 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
435 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
436 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
437 val t = rewrit @{thm Moment_Neigung} t;
438 if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
439 else error "Moment_Neigung broken";
440 (* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
441 before declaring "y''" as a constant *)
443 val t = rewrit @{thm make_fun_explicit} t;
444 if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
445 else error "make_fun_explicit broken";
448 "----------- simplify_leaf for this script -----------------------";
449 "----------- simplify_leaf for this script -----------------------";
450 "----------- simplify_leaf for this script -----------------------";
451 val srls = Rls {id="srls_IntegrierenUnd..",
453 rew_ord = ("termlessI",termlessI),
454 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
455 [(*for asm in NTH_CONS ...*)
456 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
457 (*2nd NTH_CONS pushes n+-1 into asms*)
458 Calc("Groups.plus_class.plus", eval_binop "#add_")
460 srls = Erls, calc = [], errpatts = [],
461 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
462 Calc("Groups.plus_class.plus", eval_binop "#add_"),
463 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
464 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
465 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
466 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
469 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
470 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
471 val SOME (e1__,_) = rewrite_set_ thy false srls
472 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
473 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
476 rewrite_set_ thy false srls
477 (str2term"argument_in (lhs (M_b 0 = 0))");
478 if term2str x1__ = "0" then ()
479 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
481 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
482 trace_rewrite:=false;
485 "----------- Bsp 7.27 me -----------------------------------------";
486 "----------- Bsp 7.27 me -----------------------------------------";
487 "----------- Bsp 7.27 me -----------------------------------------";
488 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
489 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
490 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
491 "FunktionsVariable x"];
493 ("Biegelinie",["MomentBestimmte","Biegelinien"],
494 ["IntegrierenUndKonstanteBestimmen"]);
495 val p = e_pos'; val c = [];
496 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
497 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
498 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
499 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
500 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
501 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
504 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
505 (*if itms2str_ ctxt pits = ... all 5 model-items*)
506 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
507 if itms2str_ ctxt mits = "[]" then ()
508 else error "biegelinie.sml: Bsp 7.27 #2";
510 val (p,_,f,nxt,_,pt) = me nxt p c pt;
511 case nxt of (_,Add_Given "FunktionsVariable x") => ()
512 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
514 val (p,_,f,nxt,_,pt) = me nxt p c pt;
515 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
516 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
517 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
518 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
520 "===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
521 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
522 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
523 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
524 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
529 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
530 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
531 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
532 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
533 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
535 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
536 | _ => error "biegelinie.sml: Bsp 7.27 #5";
537 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
538 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
539 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
541 ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
542 | _ => error "biegelinie.sml: Bsp 7.27 #5a";
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
548 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
549 | _ => error "biegelinie.sml: Bsp 7.27 #5b";
551 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
552 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
553 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
554 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
555 case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
556 | _ => error "biegelinie.sml: Bsp 7.27 #6";
558 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
559 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
561 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
562 case nxt of (_, Substitute ["x = 0"]) => ()
563 | _ => error "biegelinie.sml: Bsp 7.27 #7";
566 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
567 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
568 if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
569 else error "biegelinie.sml: Bsp 7.27 #8";
571 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
572 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
573 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
575 if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
576 else error "biegelinie.sml: Bsp 7.27 #9";
581 (*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
582 val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 "~~~~~ fun xxx, args:"; val () = ();
587 "~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
588 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
590 (*step p ((pt, Ctree.e_pos'),[]) Theory loader: undefined entry for theory "Isac.Pure"*)
591 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));
592 val pIopt = get_pblID (pt,ip);
593 ip = ([], Ctree.Res) = false;
596 member op = [Ctree.Pbl, Ctree.Met] p_
597 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) = true;
598 (*nxt_specify_ (pt, ip) Theory loader: undefined entry for theory "Isac.Pure"*)
599 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, (p, p_))) = ((pt, ip));
600 val pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
601 probl, spec = (dI, pI, mI), ...}) = Ctree.get_obj I pt p;
602 Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin = false;
603 val cpI = if pI = e_pblID then pI' else pI;
604 val cmI = if mI = e_metID then mI' else mI;
605 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
606 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
607 val pb = foldl and_ (true, map fst pre);
609 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
610 tac (*Add_Given "equalities\n [0 = c_2 +..*);
612 (*Chead.nxt_specif tac ptp Theory loader: undefined entry for theory "Isac.Pure"*)
613 "~~~~~ fun nxt_specif, args:"; val ((Tac.Add_Given ct), ptp) = (tac, ptp);
614 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, (ptp as (pt, (p, Pbl)))) = ( "#Given", ct, ptp);
615 val PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} = get_obj I pt p;
616 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
617 val cpI = if pI = e_pblID then pI' else pI;
619 val Err msg = appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct
621 ([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Isac", msg,msg,msg),
622 (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)
636 val (p,_,f,nxt,_,pt) = me nxt p c pt;
638 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
639 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
641 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
642 val (p,_,f,nxt,_,pt) = me nxt p c pt;
643 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
644 | _ => error "biegelinie.sml: Bsp 7.27 #10";
647 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
648 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
649 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
650 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
651 (*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
652 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
653 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
654 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
655 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
656 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
657 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
658 | _ => error "biegelinie.sml: Bsp 7.27 #11";
659 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
660 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
661 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
662 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
663 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
664 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
665 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
666 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
667 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
668 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
669 | _ => error "biegelinie.sml: Bsp 7.27 #12";
672 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
673 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
674 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
675 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
676 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
677 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
679 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
680 | _ => error "biegelinie.sml: Bsp 7.27 #13";
682 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
683 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
684 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
685 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
686 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
687 | _ => error "biegelinie.sml: Bsp 7.27 #14";
689 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
690 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
691 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
693 (_, Check_Postcond ["named", "integrate", "function"]) => ()
694 | _ => error "biegelinie.sml: Bsp 7.27 #15";
696 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
698 "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
699 then () else error "biegelinie.sml: Bsp 7.27 #16 f";
701 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
702 | _ => error "biegelinie.sml: Bsp 7.27 #16";
704 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
705 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
706 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
707 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
708 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
709 | _ => error "biegelinie.sml: Bsp 7.27 #17";
711 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
712 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
714 "y x =\nc_2 + c * x +\n\
715 \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
716 then () else error "biegelinie.sml: Bsp 7.27 #18 f";
718 (_, Check_Postcond ["named", "integrate", "function"]) => ()
719 | _ => error "biegelinie.sml: Bsp 7.27 #18";
721 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
722 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
723 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
724 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
725 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
726 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
729 ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
730 | _ => error "biegelinie.sml: Bsp 7.27 #19";
731 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
732 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
733 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
734 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
735 val (p,_,f,nxt,_,pt) = me nxt p c pt;
736 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
737 | _ => error "biegelinie.sml: Bsp 7.27 #20";
738 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
739 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
740 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
741 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
742 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
743 if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
744 else error "biegelinie.sml: Bsp 7.27 #21 f";
747 ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
748 | _ => error "biegelinie.sml: Bsp 7.27 #21";
749 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
750 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
751 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
752 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
753 val (p,_,f,nxt,_,pt) = me nxt p c pt;
754 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
755 | _ => error "biegelinie.sml: Bsp 7.27 #22";
756 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
757 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
758 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
759 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
760 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
761 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
762 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
763 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
764 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
765 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
766 | _ => error "biegelinie.sml: Bsp 7.27 #23";
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
770 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
771 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
772 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
774 "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
775 "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
776 then () else error "biegelinie.sml: Bsp 7.27 #24 f";
777 case nxt of ("End_Proof'", End_Proof') => ()
778 | _ => error "biegelinie.sml: Bsp 7.27 #24";
781 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
782 (([1], Frm), q_ x = q_0),
783 (([1], Res), - q_ x = - q_0),
784 (([2], Res), Q' x = - q_0),
785 (([3], Pbl), Integrate (- q_0, x)),
786 (([3,1], Frm), Q x = Integral - q_0 D x),
787 (([3,1], Res), Q x = -1 * q_0 * x + c),
788 (([3], Res), Q x = -1 * q_0 * x + c),
789 (([4], Res), M_b' x = -1 * q_0 * x + c),
790 (([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
791 (([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
792 (([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
793 (([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
794 (([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
795 (([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
796 (([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
797 (([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
798 (([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
799 (([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
800 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
801 (([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
802 (([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
803 (([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
804 (([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
805 (([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
806 (([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
807 (([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
808 (([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
809 (([10,4,4], Res), c = L * q_0 / 2),
810 (([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
811 (([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
812 (([10], Res), [c = L * q_0 / 2, c_2 = 0]),
813 (([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
814 (([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
815 (([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
816 (([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
817 (([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
818 (([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
819 (([15,1], Res), y' x =
820 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
823 "----------- Bsp 7.27 autoCalculate ------------------------------";
824 "----------- Bsp 7.27 autoCalculate ------------------------------";
825 "----------- Bsp 7.27 autoCalculate ------------------------------";
827 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
828 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
829 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
830 "FunktionsVariable x"],
832 ["MomentBestimmte","Biegelinien"],
833 ["IntegrierenUndKonstanteBestimmen"]))];
835 autoCalculate 1 CompleteCalcHead;
837 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
839 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
842 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
843 val ((pt,_),_) = get_calc 1;
844 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
845 | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
847 autoCalculate 1 CompleteCalc;
848 val ((pt,p),_) = get_calc 1;
849 if p = ([], Res) andalso length (children pt) = 23 andalso
850 term2str (get_obj g_res pt (fst p)) =
851 "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
852 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
854 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
855 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
858 (*check all formulae for getTactic*)
859 getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
860 getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
861 getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
862 getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
863 getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
864 getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
866 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
867 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
868 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
870 ["Streckenlast q_0","FunktionsVariable x",
871 "Funktionen [Q x = c + -1 * q_0 * x, \
872 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
873 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
874 \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"];
875 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
876 ["Biegelinien","ausBelastung"]);
877 val p = e_pos'; val c = [];
878 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
879 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
880 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
881 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
882 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
883 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
884 | _ => error "biegelinie.sml met2 b";
886 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
887 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
888 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
889 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
890 | _ => error "biegelinie.sml met2 c";
892 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
893 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
894 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
895 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
896 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
898 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
899 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
900 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
901 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
902 | _ => error "biegelinie.sml met2 d";
904 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
905 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
906 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
907 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
908 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
909 "M_b x = Integral c + -1 * q_0 * x D x";
910 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
911 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
912 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
913 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
914 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
915 "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
916 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
917 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
918 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
919 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
920 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
921 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
922 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
923 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
924 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
925 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
926 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
927 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
928 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
929 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
930 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
931 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
932 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
933 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
934 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
935 "y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
936 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
937 "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
938 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
939 "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
940 val (p,_,f,nxt,_,pt) = me nxt p c pt;
942 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
943 then case nxt of ("End_Proof'", End_Proof') => ()
944 | _ => error "biegelinie.sml met2 e 1"
945 else error "biegelinie.sml met2 e 2";
947 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
948 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
949 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
950 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
951 "substitution (M_b L = 0)",
953 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
954 ["Equation","fromFunction"]);
955 val p = e_pos'; val c = [];
956 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
957 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
958 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
959 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
960 val (p,_,f,nxt,_,pt) = me nxt p c pt;
962 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
963 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
964 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
965 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
966 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
967 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
968 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
969 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
970 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
971 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
972 then case nxt of ("End_Proof'", End_Proof') => ()
973 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
974 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
978 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
979 ML_file "Knowledge/algein.sml"
980 ML_file "Knowledge/diophanteq.sml"
981 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
982 ML_file "Knowledge/inssort.sml"
983 ML_file "Knowledge/isac.sml"
984 ML_file "Knowledge/build_thydata.sml"
985 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
986 ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}
987 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
988 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
989 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
991 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
992 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
993 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
995 section {* history of tests *}
997 Systematic regression tests have been introduced to isac development in 2003.
998 Sanity of the regression tests suffers from updates following Isabelle development,
999 which mostly exceeded the resources available in isac's development.
1001 The survey below shall support to efficiently use the tests for isac
1002 on different Isabelle versions. Conclusion in most cases will be:
1004 !!! Use most recent tests or go back to the old notebook
1005 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1009 subsection {* isac on Isabelle2015 *}
1010 subsubsection {* Summary of development *}
1012 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
1013 This complicates Test_Isac, see "Prepare running tests" above.
1014 * Remove TTY interface.
1015 * Re-activate insertion sort.
1017 subsubsection {* State of tests: unchanged *}
1018 subsubsection {* Changesets of begin and end *}
1020 last changeset with Test_Isac 2f1b2854927a
1021 first changeset with Test_Isac ???
1024 subsection {* isac on Isabelle2014 *}
1025 subsubsection {* Summary of development *}
1027 migration from "isabelle tty" --> libisabelle
1030 subsection {* isac on Isabelle2013-2 *}
1031 subsubsection {* Summary of development *}
1033 reactivated context_thy
1035 subsubsection {* State of tests *}
1039 subsubsection {* Changesets of begin and end *}
1043 : isac on Isablle2013-2
1045 Changeset: 55318 (03826ceb24da) merged
1046 User: Walther Neuper <neuper@ist.tugraz.at>
1047 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
1050 subsection {* isac on Isabelle2013-1 *}
1051 subsubsection {* Summary of development *}
1053 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
1054 no significant development steps for ISAC.
1056 subsubsection {* State of tests *}
1058 See points in subsection "isac on Isabelle2011", "State of tests".
1060 subsubsection {* Changesets of begin and end *}
1062 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
1063 User: Walther Neuper <neuper@ist.tugraz.at>
1064 Date: 2013-12-03 18:13:31 +0100 (8 days)
1066 : isac on Isablle2013-1
1068 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
1069 User: Walther Neuper <neuper@ist.tugraz.at>
1070 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
1074 subsection {* isac on Isabelle2013 *}
1075 subsubsection {* Summary of development *}
1077 # Oct.13: replaced "axioms" by "axiomatization"
1078 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
1079 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
1080 simplification of multivariate rationals (without improving the rulesets involved).
1082 subsubsection {* Run tests *}
1084 Is standard now; this subsection will be discontinued under Isabelle2013-1
1086 subsubsection {* State of tests *}
1088 See points in subsection "isac on Isabelle2011", "State of tests".
1089 # re-activated listC.sml
1091 subsubsection {* Changesets of begin and end *}
1093 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
1094 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
1095 Date: Tue Nov 19 22:23:30 2013 +0000
1097 : isac on Isablle2013
1099 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
1100 User: Walther Neuper <neuper@ist.tugraz.at>
1101 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
1104 subsection {* isac on Isabelle2012 *}
1105 subsubsection {* Summary of development *}
1107 isac on Isabelle2012 is considered just a transitional stage
1108 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
1109 For considerations on the transition see
1110 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
1112 subsubsection {* Run tests *}
1114 $ cd /usr/local/isabisac12/
1115 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
1116 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
1118 subsubsection {* State of tests *}
1120 At least the tests from isac on Isabelle2011 run again.
1121 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
1122 in parallel with evaluation.
1124 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
1125 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
1126 (i.e. on the old notebook from 2002).
1128 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
1129 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
1130 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
1131 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
1132 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
1134 Some tests have been re-activated (e.g. error patterns, fill patterns).
1136 subsubsection {* Changesets of begin and end *}
1138 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
1139 User: Walther Neuper <neuper@ist.tugraz.at>
1140 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
1142 : isac on Isablle2012
1144 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
1145 User: Walther Neuper <neuper@ist.tugraz.at>
1146 Date: 2012-09-24 18:35:13 +0200 (8 months)
1147 ------------------------------------------------------------------------------
1148 Changeset: 48756 (7443906996a8) merged
1149 User: Walther Neuper <neuper@ist.tugraz.at>
1150 Date: 2012-09-24 18:15:49 +0200 (8 months)
1153 subsection {* isac on Isabelle2011 *}
1154 subsubsection {* Summary of development *}
1156 isac's mathematics engine has been extended by two developments:
1157 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
1158 (2) Z_Transform was introduced by Jan Rocnik, which revealed
1159 further errors introduced by (1).
1160 (3) "error patterns" were introduced by Gabriella Daroczy
1161 Regressions tests have been added for all of these.
1163 subsubsection {* Run tests *}
1165 $ cd /usr/local/isabisac11/
1166 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
1167 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
1169 subsubsection {* State of tests *}
1171 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
1172 and sometimes give reasons for failing tests.
1173 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
1174 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
1176 The most signification tests (in particular Frontend/interface.sml) run,
1177 however, many "error in kernel" are not caught by an exception.
1178 ------------------------------------------------------------------------------
1179 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
1180 ------------------------------------------------------------------------------
1181 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
1182 User: Walther Neuper <neuper@ist.tugraz.at>
1183 Date: 2012-08-06 10:38:11 +0200 (11 months)
1186 The list below records TODOs while producing an ISAC kernel for
1187 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
1188 (so to be resumed with Isabelle2013-1):
1189 ############## WNxxxxxx.TODO can be found in sources ##############
1190 --------------------------------------------------------------------------------
1191 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
1192 --------------------------------------------------------------------------------
1193 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
1194 this special case (see) --- why not nxt = Model_Problem here ? ---
1195 --------------------------------------------------------------------------------
1196 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
1198 # simplify_* , *_simp_*
1200 # calc_* , calculate_* ... require iteration over all rls ...
1201 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
1202 --------------------------------------------------------------------------------
1203 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
1204 --------------------------------------------------------------------------------
1205 WN120314 changeset a393bb9f5e9f drops root equations.
1206 see test/Tools/isac/Knowledge/rootrateq.sml
1207 --------------------------------------------------------------------------------
1208 WN120317.TODO changeset 977788dfed26 dropped rateq:
1209 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
1210 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
1211 investigation Check_elementwise stopped due to too much effort finding out,
1212 why Check_elementwise worked in 2002 in spite of the error.
1213 --------------------------------------------------------------------------------
1214 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
1215 --------------------------------------------------------------------------------
1216 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
1217 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
1218 --------------------------------------------------------------------------------
1219 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
1220 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
1221 --------------------------------------------------------------------------------
1222 WN120320.TODO check-improve rlsthmsNOTisac:
1223 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
1224 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
1225 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
1226 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
1227 --------------------------------------------------------------------------------
1228 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
1229 --------------------------------------------------------------------------------
1230 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
1231 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
1232 --------------------------------------------------------------------------------
1233 WN120321.TODO rearrange theories:
1237 ///Descript.thy --> ProgLang
1238 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
1239 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
1240 Interpret.thy are generated (simplifies xml structure for theories)
1243 ListC.thy <--- first_Proglang_thy
1244 --------------------------------------------------------------------------------
1245 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
1246 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
1247 broken during work on thy-hierarchy
1248 --------------------------------------------------------------------------------
1249 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
1250 test --- the_hier (get_thes ()) (collect_thydata ())---
1251 --------------------------------------------------------------------------------
1252 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
1253 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
1254 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
1255 --------------------------------------------------------------------------------
1256 WN120409.TODO replace "op mem" (2002) with member (2011) ...
1257 ... an exercise interesting for beginners !
1258 --------------------------------------------------------------------------------
1259 WN120411 scanning html representation of newly generated knowledge:
1261 ** Theorems: only "Proof of the theorem" (correct!)
1262 and "(c) isac-team (math-autor)"
1263 ** Rulesets: only "Identifier:///"
1264 and "(c) isac-team (math-autor)"
1265 ** IsacKnowledge: link to dependency graph (which needs to be created first)
1266 ** IsacScripts --> ProgramLanguage
1267 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
1272 ** Z-Transform is missing !!!
1273 ** type-constraints !!!
1274 --------------------------------------------------------------------------------
1275 WN120417: merging xmldata revealed:
1276 ..............NEWLY generated:........................................
1278 <GUH> thy_isab_Fun-thm-o_apply </GUH>
1280 <STRING> Isabelle </STRING>
1281 <STRING> Fun </STRING>
1282 <STRING> Theorems </STRING>
1283 <STRING> o_apply </STRING>
1286 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
1289 <TEXT> Proof of the theorem </TEXT>
1290 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
1293 <EXPLANATIONS> </EXPLANATIONS>
1295 <STRING> Isabelle team, TU Munich </STRING>
1300 ..............OLD FORMAT:.............................................
1302 <GUH> thy_isab_Fun-thm-o_apply </GUH>
1304 <STRING> Isabelle </STRING>
1305 <STRING> Fun </STRING>
1306 <STRING> Theorems </STRING>
1307 <STRING> o_apply </STRING>
1312 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
1317 <TEXT> Proof of the theorem </TEXT>
1318 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
1321 <EXPLANATIONS> </EXPLANATIONS>
1323 <STRING> Isabelle team, TU Munich </STRING>
1328 --------------------------------------------------------------------------------
1330 subsubsection {* Changesets of begin and end *}
1332 isac development was done between these changesets:
1333 ------------------------------------------------------------------------------
1334 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
1335 User: Walther Neuper <neuper@ist.tugraz.at>
1336 Date: 2012-09-24 16:39:30 +0200 (8 months)
1338 : isac on Isablle2011
1340 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
1341 Branch: decompose-isar
1342 User: Walther Neuper <neuper@ist.tugraz.at>
1343 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
1344 ------------------------------------------------------------------------------
1347 subsection {* isac on Isabelle2009-2 *}
1348 subsubsection {* Summary of development *}
1350 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
1351 The update was painful (bridging 7 years of Isabelle development) and cut short
1352 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
1353 going on to Isabelle2011 although most of the tests did not run.
1355 subsubsection {* Run tests *}
1357 WN131021 this is broken by installation of Isabelle2011/12/13,
1358 because all these write their binaries to ~/.isabelle/heaps/..
1360 $ cd /usr/local/isabisac09-2/
1361 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
1362 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
1363 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
1365 subsubsection {* State of tests *}
1367 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
1369 subsubsection {* Changesets of begin and end *}
1371 isac development was done between these changesets:
1372 ------------------------------------------------------------------------------
1373 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
1374 Branch: decompose-isar
1375 User: Marco Steger <m.steger@student.tugraz.at>
1376 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
1378 : isac on Isablle2009-2
1380 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
1381 Branch: isac-from-Isabelle2009-2
1382 User: Walther Neuper <neuper@ist.tugraz.at>
1383 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
1384 ------------------------------------------------------------------------------
1387 subsection {* isac on Isabelle2002 *}
1388 subsubsection {* Summary of development *}
1390 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
1391 of isac's mathematics engine has been implemented.
1393 subsubsection {* Run tests *}
1394 subsubsection {* State of tests *}
1396 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
1397 recent Linux versions)
1399 subsubsection {* Changesets of begin and end *}
1401 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
1402 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
1406 (*========== inhibit exn 130719 Isabelle2013 ===================================
1407 ============ inhibit exn 130719 Isabelle2013 =================================*)
1409 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1410 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)