TermC: prep. comparing tests isabisac <--> isabisac15
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"
297 "~~~~~ fun xxx, args:"; val () = ();
302 val thy = @{theory "Isac"};
304 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
306 "----- stepwise from the rulesets in simplify_Integral and below-----";
307 val rls = norm_Rational_noadd_fractions;
308 case rewrite_set_inst_ thy true subs rls t of
309 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
313 val rls = order_add_mult_in;
314 val SOME (t,[]) = rewrite_set_ thy true rls t;
315 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
316 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
319 val rls = discard_parentheses;
320 val SOME (t,[]) = rewrite_set_ thy true rls t;
321 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
322 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
326 (append_rls "separate_bdv" collect_bdv
327 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
328 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
329 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
330 (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
331 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
332 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
333 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
334 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
336 (*show_types := true; --- do we need type-constraint in thms? *)
337 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
338 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
339 @{thm separate_1_bdv}; (*::?'a*)
340 val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
341 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
342 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
345 "~~~~~ fun xxx, args:"; val () = ();
346 (*//==========================================================================================\\*)
352 (*\\==========================================================================================//*)
353 "~~~~~ fun xxx, args:"; val () = ();
355 (* isabisac <> isabisac15 *)
356 (*val SOME (t, []) = rewrite_set_inst_ thy true subs rls t; isabisac15 *)
357 val NONE = rewrite_set_inst_ thy true subs rls t; (* isabisac *)
359 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
360 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
371 ML_file "Knowledge/eqsystem.sml"
372 ML_file "Knowledge/test.sml"
373 ML_file "Knowledge/polyminus.sml"
374 ML_file "Knowledge/vect.sml"
375 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
376 ML_file "Knowledge/biegelinie-1.sml"
380 (* tests on biegelinie
381 author: Walther Neuper 050826
382 (c) due to copyright terms
385 trace_rewrite := false;
386 "-----------------------------------------------------------------";
387 "table of contents -----------------------------------------------";
388 "-----------------------------------------------------------------";
389 "----------- the rules -------------------------------------------";
390 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
391 "----------- simplify_leaf for this script -----------------------";
392 "----------- Bsp 7.27 me -----------------------------------------";
393 "----------- Bsp 7.27 autoCalculate ------------------------------";
394 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
395 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
396 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
397 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
398 "----------- investigate normalforms in biegelinien --------------";
399 "-----------------------------------------------------------------";
400 "-----------------------------------------------------------------";
401 "-----------------------------------------------------------------";
403 val thy = @{theory "Biegelinie"};
404 val ctxt = thy2ctxt' "Biegelinie";
405 fun str2term str = (Thm.term_of o the o (parse thy)) str;
406 fun term2s t = term_to_string'' "Biegelinie" t;
408 fst (the (rewrite_ thy tless_true e_rls true thm str));
411 "----------- the rules -------------------------------------------";
412 "----------- the rules -------------------------------------------";
413 "----------- the rules -------------------------------------------";
414 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
415 if term2s t = "Q' x = - q_0" then ()
416 else error "/biegelinie.sml: Belastung_Querkraft";
418 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
419 if term2s t = "M_b' x = - q_0 * x + c" then ()
420 else error "/biegelinie.sml: Querkraft_Moment";
422 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
424 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
425 else error "biegelinie.sml: Moment_Neigung";
428 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
429 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
430 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
431 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
432 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
433 val t = rewrit @{thm Moment_Neigung} t;
434 if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
435 else error "Moment_Neigung broken";
436 (* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
437 before declaring "y''" as a constant *)
439 val t = rewrit @{thm make_fun_explicit} t;
440 if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
441 else error "make_fun_explicit broken";
444 "----------- simplify_leaf for this script -----------------------";
445 "----------- simplify_leaf for this script -----------------------";
446 "----------- simplify_leaf for this script -----------------------";
447 val srls = Rls {id="srls_IntegrierenUnd..",
449 rew_ord = ("termlessI",termlessI),
450 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
451 [(*for asm in NTH_CONS ...*)
452 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
453 (*2nd NTH_CONS pushes n+-1 into asms*)
454 Calc("Groups.plus_class.plus", eval_binop "#add_")
456 srls = Erls, calc = [], errpatts = [],
457 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
458 Calc("Groups.plus_class.plus", eval_binop "#add_"),
459 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
460 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
461 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
462 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
465 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
466 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
467 val SOME (e1__,_) = rewrite_set_ thy false srls
468 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
469 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
472 rewrite_set_ thy false srls
473 (str2term"argument_in (lhs (M_b 0 = 0))");
474 if term2str x1__ = "0" then ()
475 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
477 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
478 trace_rewrite:=false;
481 "----------- Bsp 7.27 me -----------------------------------------";
482 "----------- Bsp 7.27 me -----------------------------------------";
483 "----------- Bsp 7.27 me -----------------------------------------";
484 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
485 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
486 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
487 "FunktionsVariable x"];
489 ("Biegelinie",["MomentBestimmte","Biegelinien"],
490 ["IntegrierenUndKonstanteBestimmen"]);
491 val p = e_pos'; val c = [];
492 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
493 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
494 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
495 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
496 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
497 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
500 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
501 (*if itms2str_ ctxt pits = ... all 5 model-items*)
502 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
503 if itms2str_ ctxt mits = "[]" then ()
504 else error "biegelinie.sml: Bsp 7.27 #2";
506 val (p,_,f,nxt,_,pt) = me nxt p c pt;
507 case nxt of (_,Add_Given "FunktionsVariable x") => ()
508 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
510 val (p,_,f,nxt,_,pt) = me nxt p c pt;
511 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
512 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
513 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
514 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
516 "===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
517 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
518 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
519 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
520 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
521 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
525 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
526 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
531 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
532 | _ => error "biegelinie.sml: Bsp 7.27 #5";
533 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
534 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
535 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
537 ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
538 | _ => error "biegelinie.sml: Bsp 7.27 #5a";
541 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
542 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
544 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
545 | _ => error "biegelinie.sml: Bsp 7.27 #5b";
547 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
548 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
549 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
550 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
551 case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
552 | _ => error "biegelinie.sml: Bsp 7.27 #6";
554 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
555 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
557 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
558 case nxt of (_, Substitute ["x = 0"]) => ()
559 | _ => error "biegelinie.sml: Bsp 7.27 #7";
562 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
563 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
564 if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
565 else error "biegelinie.sml: Bsp 7.27 #8";
567 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
568 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
569 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
571 if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
572 else error "biegelinie.sml: Bsp 7.27 #9";
577 (*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
578 val (p,_,f,nxt,_,pt) = me nxt p c pt;
582 "~~~~~ fun xxx, args:"; val () = ();
583 "~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
584 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
586 (*step p ((pt, Ctree.e_pos'),[]) Theory loader: undefined entry for theory "Isac.Pure"*)
587 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));
588 val pIopt = get_pblID (pt,ip);
589 ip = ([], Ctree.Res) = false;
592 member op = [Ctree.Pbl, Ctree.Met] p_
593 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) = true;
594 (*nxt_specify_ (pt, ip) Theory loader: undefined entry for theory "Isac.Pure"*)
595 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, (p, p_))) = ((pt, ip));
596 val pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
597 probl, spec = (dI, pI, mI), ...}) = Ctree.get_obj I pt p;
598 Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin = false;
599 val cpI = if pI = e_pblID then pI' else pI;
600 val cmI = if mI = e_metID then mI' else mI;
601 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
602 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
603 val pb = foldl and_ (true, map fst pre);
605 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
606 tac (*Add_Given "equalities\n [0 = c_2 +..*);
608 (*Chead.nxt_specif tac ptp Theory loader: undefined entry for theory "Isac.Pure"*)
609 "~~~~~ fun nxt_specif, args:"; val ((Tac.Add_Given ct), ptp) = (tac, ptp);
610 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, (ptp as (pt, (p, Pbl)))) = ( "#Given", ct, ptp);
611 val PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} = get_obj I pt p;
612 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
613 val cpI = if pI = e_pblID then pI' else pI;
615 val Err msg = appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct
617 ([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Isac", msg,msg,msg),
618 (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)
632 val (p,_,f,nxt,_,pt) = me nxt p c pt;
634 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
635 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
637 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
638 val (p,_,f,nxt,_,pt) = me nxt p c pt;
639 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
640 | _ => error "biegelinie.sml: Bsp 7.27 #10";
643 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
644 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
645 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
646 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
647 (*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
648 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
649 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
650 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
651 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
652 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
653 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
654 | _ => error "biegelinie.sml: Bsp 7.27 #11";
655 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
656 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
657 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
658 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
665 | _ => error "biegelinie.sml: Bsp 7.27 #12";
668 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
669 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
670 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
671 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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;
675 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
676 | _ => error "biegelinie.sml: Bsp 7.27 #13";
678 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
679 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
680 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
681 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
682 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
683 | _ => error "biegelinie.sml: Bsp 7.27 #14";
685 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
686 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
687 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
689 (_, Check_Postcond ["named", "integrate", "function"]) => ()
690 | _ => error "biegelinie.sml: Bsp 7.27 #15";
692 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
694 "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
695 then () else error "biegelinie.sml: Bsp 7.27 #16 f";
697 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
698 | _ => error "biegelinie.sml: Bsp 7.27 #16";
700 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
701 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
702 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
703 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
704 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
705 | _ => error "biegelinie.sml: Bsp 7.27 #17";
707 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
708 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
710 "y x =\nc_2 + c * x +\n\
711 \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
712 then () else error "biegelinie.sml: Bsp 7.27 #18 f";
714 (_, Check_Postcond ["named", "integrate", "function"]) => ()
715 | _ => error "biegelinie.sml: Bsp 7.27 #18";
717 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
718 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
719 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
720 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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;
725 ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
726 | _ => error "biegelinie.sml: Bsp 7.27 #19";
727 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
728 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
729 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
730 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
731 val (p,_,f,nxt,_,pt) = me nxt p c pt;
732 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
733 | _ => error "biegelinie.sml: Bsp 7.27 #20";
734 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
735 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
736 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
737 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
738 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
739 if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
740 else error "biegelinie.sml: Bsp 7.27 #21 f";
743 ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
744 | _ => error "biegelinie.sml: Bsp 7.27 #21";
745 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
746 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
747 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
748 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
749 val (p,_,f,nxt,_,pt) = me nxt p c pt;
750 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
751 | _ => error "biegelinie.sml: Bsp 7.27 #22";
752 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
753 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
754 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
755 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
762 | _ => error "biegelinie.sml: Bsp 7.27 #23";
764 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
765 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
766 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
770 "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
771 "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
772 then () else error "biegelinie.sml: Bsp 7.27 #24 f";
773 case nxt of ("End_Proof'", End_Proof') => ()
774 | _ => error "biegelinie.sml: Bsp 7.27 #24";
777 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
778 (([1], Frm), q_ x = q_0),
779 (([1], Res), - q_ x = - q_0),
780 (([2], Res), Q' x = - q_0),
781 (([3], Pbl), Integrate (- q_0, x)),
782 (([3,1], Frm), Q x = Integral - q_0 D x),
783 (([3,1], Res), Q x = -1 * q_0 * x + c),
784 (([3], Res), Q x = -1 * q_0 * x + c),
785 (([4], Res), M_b' x = -1 * q_0 * x + c),
786 (([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
787 (([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
788 (([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
789 (([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
790 (([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
791 (([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
792 (([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
793 (([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
794 (([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
795 (([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
796 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
797 (([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
798 (([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
799 (([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
800 (([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
801 (([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
802 (([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
803 (([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
804 (([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
805 (([10,4,4], Res), c = L * q_0 / 2),
806 (([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
807 (([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
808 (([10], Res), [c = L * q_0 / 2, c_2 = 0]),
809 (([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
810 (([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
811 (([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
812 (([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
813 (([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
814 (([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
815 (([15,1], Res), y' x =
816 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
819 "----------- Bsp 7.27 autoCalculate ------------------------------";
820 "----------- Bsp 7.27 autoCalculate ------------------------------";
821 "----------- Bsp 7.27 autoCalculate ------------------------------";
823 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
824 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
825 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
826 "FunktionsVariable x"],
828 ["MomentBestimmte","Biegelinien"],
829 ["IntegrierenUndKonstanteBestimmen"]))];
831 autoCalculate 1 CompleteCalcHead;
833 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
835 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
838 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
839 val ((pt,_),_) = get_calc 1;
840 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
841 | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
843 autoCalculate 1 CompleteCalc;
844 val ((pt,p),_) = get_calc 1;
845 if p = ([], Res) andalso length (children pt) = 23 andalso
846 term2str (get_obj g_res pt (fst p)) =
847 "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)"
848 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
850 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
851 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
854 (*check all formulae for getTactic*)
855 getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
856 getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
857 getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
858 getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
859 getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
860 getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
862 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
863 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
864 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
866 ["Streckenlast q_0","FunktionsVariable x",
867 "Funktionen [Q x = c + -1 * q_0 * x, \
868 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
869 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
870 \ 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)]"];
871 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
872 ["Biegelinien","ausBelastung"]);
873 val p = e_pos'; val c = [];
874 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
875 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
876 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
877 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
878 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
879 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
880 | _ => error "biegelinie.sml met2 b";
882 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
883 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
884 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
885 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
886 | _ => error "biegelinie.sml met2 c";
888 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
889 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
890 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
891 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
892 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; f2str f = "Q x = c + -1 * q_0 * x";
895 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
896 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
897 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
898 | _ => error "biegelinie.sml met2 d";
900 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
901 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
902 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
903 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
904 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
905 "M_b x = Integral c + -1 * q_0 * x D x";
906 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
907 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
908 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
909 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
910 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
911 "- EI * y'' 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 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
914 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
915 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
916 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
917 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
918 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
919 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
920 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
921 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
922 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
923 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
924 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
925 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
926 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
927 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
928 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
929 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
930 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
931 "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";
932 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
933 "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)";
934 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
935 "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)";
936 val (p,_,f,nxt,_,pt) = me nxt p c pt;
938 "[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)]"
939 then case nxt of ("End_Proof'", End_Proof') => ()
940 | _ => error "biegelinie.sml met2 e 1"
941 else error "biegelinie.sml met2 e 2";
943 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
944 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
945 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
946 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
947 "substitution (M_b L = 0)",
949 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
950 ["Equation","fromFunction"]);
951 val p = e_pos'; val c = [];
952 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
953 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
954 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
955 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
956 val (p,_,f,nxt,_,pt) = me nxt p c pt;
958 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
959 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
960 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
961 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
962 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
963 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
964 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
965 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
966 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
967 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
968 then case nxt of ("End_Proof'", End_Proof') => ()
969 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
970 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
974 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
975 ML_file "Knowledge/algein.sml"
976 ML_file "Knowledge/diophanteq.sml"
977 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
978 ML_file "Knowledge/inssort.sml"
979 ML_file "Knowledge/isac.sml"
980 ML_file "Knowledge/build_thydata.sml"
981 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
982 ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}
983 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
984 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
985 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
987 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
988 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
989 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
991 section {* history of tests *}
993 Systematic regression tests have been introduced to isac development in 2003.
994 Sanity of the regression tests suffers from updates following Isabelle development,
995 which mostly exceeded the resources available in isac's development.
997 The survey below shall support to efficiently use the tests for isac
998 on different Isabelle versions. Conclusion in most cases will be:
1000 !!! Use most recent tests or go back to the old notebook
1001 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1005 subsection {* isac on Isabelle2015 *}
1006 subsubsection {* Summary of development *}
1008 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
1009 This complicates Test_Isac, see "Prepare running tests" above.
1010 * Remove TTY interface.
1011 * Re-activate insertion sort.
1013 subsubsection {* State of tests: unchanged *}
1014 subsubsection {* Changesets of begin and end *}
1016 last changeset with Test_Isac 2f1b2854927a
1017 first changeset with Test_Isac ???
1020 subsection {* isac on Isabelle2014 *}
1021 subsubsection {* Summary of development *}
1023 migration from "isabelle tty" --> libisabelle
1026 subsection {* isac on Isabelle2013-2 *}
1027 subsubsection {* Summary of development *}
1029 reactivated context_thy
1031 subsubsection {* State of tests *}
1035 subsubsection {* Changesets of begin and end *}
1039 : isac on Isablle2013-2
1041 Changeset: 55318 (03826ceb24da) merged
1042 User: Walther Neuper <neuper@ist.tugraz.at>
1043 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
1046 subsection {* isac on Isabelle2013-1 *}
1047 subsubsection {* Summary of development *}
1049 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
1050 no significant development steps for ISAC.
1052 subsubsection {* State of tests *}
1054 See points in subsection "isac on Isabelle2011", "State of tests".
1056 subsubsection {* Changesets of begin and end *}
1058 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
1059 User: Walther Neuper <neuper@ist.tugraz.at>
1060 Date: 2013-12-03 18:13:31 +0100 (8 days)
1062 : isac on Isablle2013-1
1064 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
1065 User: Walther Neuper <neuper@ist.tugraz.at>
1066 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
1070 subsection {* isac on Isabelle2013 *}
1071 subsubsection {* Summary of development *}
1073 # Oct.13: replaced "axioms" by "axiomatization"
1074 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
1075 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
1076 simplification of multivariate rationals (without improving the rulesets involved).
1078 subsubsection {* Run tests *}
1080 Is standard now; this subsection will be discontinued under Isabelle2013-1
1082 subsubsection {* State of tests *}
1084 See points in subsection "isac on Isabelle2011", "State of tests".
1085 # re-activated listC.sml
1087 subsubsection {* Changesets of begin and end *}
1089 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
1090 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
1091 Date: Tue Nov 19 22:23:30 2013 +0000
1093 : isac on Isablle2013
1095 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
1096 User: Walther Neuper <neuper@ist.tugraz.at>
1097 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
1100 subsection {* isac on Isabelle2012 *}
1101 subsubsection {* Summary of development *}
1103 isac on Isabelle2012 is considered just a transitional stage
1104 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
1105 For considerations on the transition see
1106 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
1108 subsubsection {* Run tests *}
1110 $ cd /usr/local/isabisac12/
1111 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
1112 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
1114 subsubsection {* State of tests *}
1116 At least the tests from isac on Isabelle2011 run again.
1117 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
1118 in parallel with evaluation.
1120 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
1121 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
1122 (i.e. on the old notebook from 2002).
1124 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
1125 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
1126 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
1127 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
1128 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
1130 Some tests have been re-activated (e.g. error patterns, fill patterns).
1132 subsubsection {* Changesets of begin and end *}
1134 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
1135 User: Walther Neuper <neuper@ist.tugraz.at>
1136 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
1138 : isac on Isablle2012
1140 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
1141 User: Walther Neuper <neuper@ist.tugraz.at>
1142 Date: 2012-09-24 18:35:13 +0200 (8 months)
1143 ------------------------------------------------------------------------------
1144 Changeset: 48756 (7443906996a8) merged
1145 User: Walther Neuper <neuper@ist.tugraz.at>
1146 Date: 2012-09-24 18:15:49 +0200 (8 months)
1149 subsection {* isac on Isabelle2011 *}
1150 subsubsection {* Summary of development *}
1152 isac's mathematics engine has been extended by two developments:
1153 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
1154 (2) Z_Transform was introduced by Jan Rocnik, which revealed
1155 further errors introduced by (1).
1156 (3) "error patterns" were introduced by Gabriella Daroczy
1157 Regressions tests have been added for all of these.
1159 subsubsection {* Run tests *}
1161 $ cd /usr/local/isabisac11/
1162 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
1163 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
1165 subsubsection {* State of tests *}
1167 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
1168 and sometimes give reasons for failing tests.
1169 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
1170 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
1172 The most signification tests (in particular Frontend/interface.sml) run,
1173 however, many "error in kernel" are not caught by an exception.
1174 ------------------------------------------------------------------------------
1175 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
1176 ------------------------------------------------------------------------------
1177 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
1178 User: Walther Neuper <neuper@ist.tugraz.at>
1179 Date: 2012-08-06 10:38:11 +0200 (11 months)
1182 The list below records TODOs while producing an ISAC kernel for
1183 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
1184 (so to be resumed with Isabelle2013-1):
1185 ############## WNxxxxxx.TODO can be found in sources ##############
1186 --------------------------------------------------------------------------------
1187 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
1188 --------------------------------------------------------------------------------
1189 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
1190 this special case (see) --- why not nxt = Model_Problem here ? ---
1191 --------------------------------------------------------------------------------
1192 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
1194 # simplify_* , *_simp_*
1196 # calc_* , calculate_* ... require iteration over all rls ...
1197 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
1198 --------------------------------------------------------------------------------
1199 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
1200 --------------------------------------------------------------------------------
1201 WN120314 changeset a393bb9f5e9f drops root equations.
1202 see test/Tools/isac/Knowledge/rootrateq.sml
1203 --------------------------------------------------------------------------------
1204 WN120317.TODO changeset 977788dfed26 dropped rateq:
1205 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
1206 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
1207 investigation Check_elementwise stopped due to too much effort finding out,
1208 why Check_elementwise worked in 2002 in spite of the error.
1209 --------------------------------------------------------------------------------
1210 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
1211 --------------------------------------------------------------------------------
1212 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
1213 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
1214 --------------------------------------------------------------------------------
1215 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
1216 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
1217 --------------------------------------------------------------------------------
1218 WN120320.TODO check-improve rlsthmsNOTisac:
1219 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
1220 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
1221 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
1222 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
1223 --------------------------------------------------------------------------------
1224 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
1225 --------------------------------------------------------------------------------
1226 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
1227 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
1228 --------------------------------------------------------------------------------
1229 WN120321.TODO rearrange theories:
1233 ///Descript.thy --> ProgLang
1234 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
1235 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
1236 Interpret.thy are generated (simplifies xml structure for theories)
1239 ListC.thy <--- first_Proglang_thy
1240 --------------------------------------------------------------------------------
1241 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
1242 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
1243 broken during work on thy-hierarchy
1244 --------------------------------------------------------------------------------
1245 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
1246 test --- the_hier (get_thes ()) (collect_thydata ())---
1247 --------------------------------------------------------------------------------
1248 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
1249 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
1250 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
1251 --------------------------------------------------------------------------------
1252 WN120409.TODO replace "op mem" (2002) with member (2011) ...
1253 ... an exercise interesting for beginners !
1254 --------------------------------------------------------------------------------
1255 WN120411 scanning html representation of newly generated knowledge:
1257 ** Theorems: only "Proof of the theorem" (correct!)
1258 and "(c) isac-team (math-autor)"
1259 ** Rulesets: only "Identifier:///"
1260 and "(c) isac-team (math-autor)"
1261 ** IsacKnowledge: link to dependency graph (which needs to be created first)
1262 ** IsacScripts --> ProgramLanguage
1263 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
1268 ** Z-Transform is missing !!!
1269 ** type-constraints !!!
1270 --------------------------------------------------------------------------------
1271 WN120417: merging xmldata revealed:
1272 ..............NEWLY generated:........................................
1274 <GUH> thy_isab_Fun-thm-o_apply </GUH>
1276 <STRING> Isabelle </STRING>
1277 <STRING> Fun </STRING>
1278 <STRING> Theorems </STRING>
1279 <STRING> o_apply </STRING>
1282 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
1285 <TEXT> Proof of the theorem </TEXT>
1286 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
1289 <EXPLANATIONS> </EXPLANATIONS>
1291 <STRING> Isabelle team, TU Munich </STRING>
1296 ..............OLD FORMAT:.............................................
1298 <GUH> thy_isab_Fun-thm-o_apply </GUH>
1300 <STRING> Isabelle </STRING>
1301 <STRING> Fun </STRING>
1302 <STRING> Theorems </STRING>
1303 <STRING> o_apply </STRING>
1308 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
1313 <TEXT> Proof of the theorem </TEXT>
1314 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
1317 <EXPLANATIONS> </EXPLANATIONS>
1319 <STRING> Isabelle team, TU Munich </STRING>
1324 --------------------------------------------------------------------------------
1326 subsubsection {* Changesets of begin and end *}
1328 isac development was done between these changesets:
1329 ------------------------------------------------------------------------------
1330 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
1331 User: Walther Neuper <neuper@ist.tugraz.at>
1332 Date: 2012-09-24 16:39:30 +0200 (8 months)
1334 : isac on Isablle2011
1336 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
1337 Branch: decompose-isar
1338 User: Walther Neuper <neuper@ist.tugraz.at>
1339 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
1340 ------------------------------------------------------------------------------
1343 subsection {* isac on Isabelle2009-2 *}
1344 subsubsection {* Summary of development *}
1346 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
1347 The update was painful (bridging 7 years of Isabelle development) and cut short
1348 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
1349 going on to Isabelle2011 although most of the tests did not run.
1351 subsubsection {* Run tests *}
1353 WN131021 this is broken by installation of Isabelle2011/12/13,
1354 because all these write their binaries to ~/.isabelle/heaps/..
1356 $ cd /usr/local/isabisac09-2/
1357 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
1358 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
1359 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
1361 subsubsection {* State of tests *}
1363 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
1365 subsubsection {* Changesets of begin and end *}
1367 isac development was done between these changesets:
1368 ------------------------------------------------------------------------------
1369 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
1370 Branch: decompose-isar
1371 User: Marco Steger <m.steger@student.tugraz.at>
1372 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
1374 : isac on Isablle2009-2
1376 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
1377 Branch: isac-from-Isabelle2009-2
1378 User: Walther Neuper <neuper@ist.tugraz.at>
1379 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
1380 ------------------------------------------------------------------------------
1383 subsection {* isac on Isabelle2002 *}
1384 subsubsection {* Summary of development *}
1386 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
1387 of isac's mathematics engine has been implemented.
1389 subsubsection {* Run tests *}
1390 subsubsection {* State of tests *}
1392 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
1393 recent Linux versions)
1395 subsubsection {* Changesets of begin and end *}
1397 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
1398 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
1402 (*========== inhibit exn 130719 Isabelle2013 ===================================
1403 ============ inhibit exn 130719 Isabelle2013 =================================*)
1405 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1406 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)