wneuper/isa: test/Tools/isac/Test

     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"

     7    plus

     8      ~~/test/Tools/isac/ADDTESTS

     9      ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality

    10 -------------------------------------------------------------------------------

    12 Prepare running tests: see below

    13 Run tests:

    14 $ cd /usr/local/isabisac/

    15 $ export ISABELLE_VERSION=2015 # for libisabelle

    16 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &

    17 *)

    19 section \<open>Prepare running tests\<close>

    20 text \<open>

    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

    41 \<close>

    43 section \<open>code for copy & paste\<close>

    44 text \<open>

    45 "~~~~~ fun , args:"; val () = ();

    46 "~~~~~ and , args:"; val () = ();

    48 "~~~~~ to  return val:"; val () = ();

    50 \<close>

    51 section \<open>Run the tests\<close>

    52 text \<open>

    53 * say "OK" to the popup asking for theories to be loaded

    54 * watch the <Theories> window for errors in the "imports" below

    55 \<close>

    57 theory Test_Isac imports Build_Thydata

    58 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)

    59   "ADDTESTS/accumulate-val/Thy_All"

    60   "ADDTESTS/Ctxt"

    61   "ADDTESTS/test-depend/Build_Test"

    62   "ADDTESTS/All_Ctxt"

    63   "ADDTESTS/Test_Units"

    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 ------------------------------/*)

    87 begin

    89 ML {*

    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      *)

    93   open Kernel;

    94   open Math_Engine;            CalcTreeTEST;

    95   open Lucin;                  appy;

    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 *)

   104   open Selem;                  e_fmz;

   105   open Stool;                  transfer_asms_from_to;

   106   open Tac;                    (* NONE *)

   107   open Model;                  (* NONE *)

   108   open LTool;                  rule2stac;

   109   open Rewrite;                mk_thm;

   110   open Calc;                   get_pair;

   111   open TermC;                  ;

   112 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

   113 *}

   115 ML {*

   116 "~~~~~ fun xxx, args:"; val () = ();

   117 *} ML {*

   118 *} ML {*

   119 *}

   121 ML {*

   122   KEStore_Elems.set_ref_thy @{theory};

   123   (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);

   124 *}

   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*)

   182 ML {*

   183 "----------- fun autoCalculate -----------------------------------";

   184 reset_states ();

   185 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)

   186     [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],

   187       ("Integrate", ["integrate", "function"], ["diff", "integration"]))];

   188 Iterator 1;

   189 moveActiveRoot 1;

   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);

   209 "----- step 1 ---";

   210 autoCalculate 1 (Step 1);

   211 "----- step 2 ---";

   212 autoCalculate 1 (Step 1);

   213 "----- step 3 ---";

   214 autoCalculate 1 (Step 1);

   215 *} ML {*

   216 "----- step 4 ---";

   217 autoCalculate 1 (Step 1);

   218 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;

   219 *} ML {*

   220 term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)";

   221 *} ML {*

   222 "----- step 5 ---";

   223 autoCalculate 1 (Step 1);

   224 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;

   225 *} ML {*

   226 term2str t;

   227 *} ML {*

   228 "----- step 6 ---";

   229 autoCalculate 1 (Step 1);

   230 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;

   231 *} ML {*

   232 term2str t;

   233 *} ML {*

   234 "----- step 7 ---";

   235 autoCalculate 1 (Step 1);

   236 val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;

   237 *} ML {*

   238 term2str t;

   239 *} ML {*

   240 "----- step 8 ---";

   241 autoCalculate 1 (Step 1);

   242 val (ptp as (_, p), _) = get_calc 1;

   243 val (Form t,_,_) = pt_extract ptp;

   245 *} ML {*

   246 *} ML {*

   247 term2str t

   248 *} ML {*

   249 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()

   250 else error "mathengine.sml -- fun autoCalculate -- end";

   251 *} ML {*

   252 *} ML {*

   253 *}

   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"

   296 ML {*

   297 *} ML {*

   298 "----------- simplify by ruleset reducing make_ratpoly_in";

   299 val thy = @{theory "Isac"};

   300 "===== test 1";

   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"

   307   | NONE => ();

   309 "===== test 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";

   315 "===== test 3";

   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";

   321 "===== test 4";

   322 val rls =

   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"*)

   332     ]);

   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";

   345 "===== test 5";

   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 ........................................";

   356 val t = str2t

   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;

   360 if term2str 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;

   366 term2str t;

   367 if term2str 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 {*

   373 *}

   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"

   382 ML {*

   383 *} ML {*

   384 (* tests on biegelinie

   385    author: Walther Neuper 050826

   386    (c) due to copyright terms

   387 *)

   388 *} ML {*

   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;

   411 fun rewrit thm str =

   412     fst (the (rewrite_ thy tless_true e_rls true thm str));

   413 *} ML {*

   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");

   427     term2s t;

   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";

   430 *} ML {*

   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";

   446 *} ML {*

   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..",

   452 		preconds = [],

   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_")

   459 				   ],

   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")

   467 			 ],

   468 		scr = EmptyScr};

   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_";

   475 val SOME (x1__,_) =

   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;

   483 *} ML {*

   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"];

   492 val (dI',pI',mI') =

   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;

   503 *} ML {*

   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;

   527 *} ML {*

   528 case nxt of

   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;

   540 case nxt of

   541     ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()

   542 	  | _ => error  "biegelinie.sml: Bsp 7.27 #5a";

   544 *} ML {*

   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;

   547 case nxt of

   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..*);

   560 f2str f;

   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";

   565 *} ML {*

   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;

   574 *} ML {*

   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";

   578 *} ML {*

   579 (*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)

   580 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   581 *} ML {*

   582 nxt;

   583 *} ML {*

   584 "~~~~~ fun xxx, args:"; val () = ();

   585 "~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);

   586 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)

   587     val (pt, p) = ptp;

   588 (*step p ((pt, Ctree.e_pos'),[]) Theory loader: undefined entry for theory "Isac.Pure"*)

   589 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));

   590 val pIopt = get_pblID (pt,ip);

   591 ip = ([], Ctree.Res) = false;

   592 tacis = [];

   593 pIopt (*SOME*);

   594 member op = [Ctree.Pbl, Ctree.Met] p_

   595   	                    andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) = true;

   596 (*nxt_specify_ (pt, ip) Theory loader: undefined entry for theory "Isac.Pure"*)

   597 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, (p, p_))) = ((pt, ip));

   598 val pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

   599   		  probl, spec = (dI, pI, mI), ...}) = Ctree.get_obj I pt p;

   600 Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin = false;

   601         val cpI = if pI = e_pblID then pI' else pI;

   602   	    val cmI = if mI = e_metID then mI' else mI;

   603   	    val {ppc, prls, where_, ...} = Specify.get_pbt cpI;

   604   	    val pre = Stool.check_preconds "thy 100820" prls where_ probl;

   605   	    val pb = foldl and_ (true, map fst pre);

   606   	    val (_, tac) =

   607   	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);

   608 tac (*Add_Given "equalities\n [0 = c_2 +..*);

   609 *} ML {*

   610 (*Chead.nxt_specif tac ptp   Theory loader: undefined entry for theory "Isac.Pure"*)

   611 "~~~~~ fun nxt_specif, args:"; val ((Tac.Add_Given ct), ptp) = (tac, ptp);

   612 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, (ptp as (pt, (p, Pbl)))) = ( "#Given", ct, ptp);

   613 val PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} = get_obj I pt p;

   614       val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

   615       val cpI = if pI = e_pblID then pI' else pI;

   616 *} ML {*

   617 val Err msg = appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct

   618 *} ML {*

   619 ([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Isac", msg,msg,msg),

   620 	          (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)

   621 *} ML {*

   622 *} ML {*

   623 *} ML {*

   624 *} ML {*

   625 *} ML {*

   626 *} ML {*

   627 *} ML {*

   628 *} ML {*

   629 *} ML {*

   630 *} ML {*

   631 *} ML {*

   632 *} ML {*

   633 *} ML {*

   634 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   635 *} ML {*

   636 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   637 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   638 *} ML {*

   639 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   640 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   641 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()

   642 	  | _ => error  "biegelinie.sml: Bsp 7.27 #10";

   644 *} ML {*

   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 (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 nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)

   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 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 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()

   656 	  | _ => error  "biegelinie.sml: Bsp 7.27 #11";

   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 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 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()

   667 	  | _ => error  "biegelinie.sml: Bsp 7.27 #12";

   669 *} ML {*

   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;

   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 case nxt of

   677     (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()

   678 	  | _ => error  "biegelinie.sml: Bsp 7.27 #13";

   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 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 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()

   685 	  | _ => error  "biegelinie.sml: Bsp 7.27 #14";

   687 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   688 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   689 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   690 case nxt of

   691     (_, Check_Postcond ["named", "integrate", "function"]) => ()

   692   | _ => error  "biegelinie.sml: Bsp 7.27 #15";

   694 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   695 if f2str f =

   696   "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

   697 then () else error  "biegelinie.sml: Bsp 7.27 #16 f";

   698 case nxt of

   699     (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()

   700 	  | _ => error  "biegelinie.sml: Bsp 7.27 #16";

   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 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 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()

   707 	  | _ => error  "biegelinie.sml: Bsp 7.27 #17";

   709 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   710 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   711 if f2str f =

   712    "y x =\nc_2 + c * x +\n\

   713    \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"

   714 then () else error  "biegelinie.sml: Bsp 7.27 #18 f";

   715 case nxt of

   716     (_, Check_Postcond ["named", "integrate", "function"]) => ()

   717   | _ => error  "biegelinie.sml: Bsp 7.27 #18";

   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;

   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 case nxt of

   726     (_, Subproblem

   727             ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()

   728   | _ => error  "biegelinie.sml: Bsp 7.27 #19";

   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;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;

   734 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()

   735 	  | _ => error  "biegelinie.sml: Bsp 7.27 #20";

   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 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 if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()

   742 else error  "biegelinie.sml: Bsp 7.27 #21 f";

   743 case nxt of

   744     (_, Subproblem

   745             ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()

   746   | _ => error  "biegelinie.sml: Bsp 7.27 #21";

   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;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;

   752 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()

   753 	  | _ => error  "biegelinie.sml: Bsp 7.27 #22";

   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 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 case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()

   764 	  | _ => error  "biegelinie.sml: Bsp 7.27 #23";

   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;

   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 if f2str f =

   772   "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^

   773   "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"

   774 then () else error  "biegelinie.sml: Bsp 7.27 #24 f";

   775 case nxt of ("End_Proof'", End_Proof') => ()

   776 	  | _ => error  "biegelinie.sml: Bsp 7.27 #24";

   778 show_pt pt;

   779 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),

   780 (([1], Frm), q_ x = q_0),

   781 (([1], Res), - q_ x = - q_0),

   782 (([2], Res), Q' x = - q_0),

   783 (([3], Pbl), Integrate (- q_0, x)),

   784 (([3,1], Frm), Q x = Integral - q_0 D x),

   785 (([3,1], Res), Q x = -1 * q_0 * x + c),

   786 (([3], Res), Q x = -1 * q_0 * x + c),

   787 (([4], Res), M_b' x = -1 * q_0 * x + c),

   788 (([5], Pbl), Integrate (-1 * q_0 * x + c, x)),

   789 (([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),

   790 (([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),

   791 (([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),

   792 (([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),

   793 (([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),

   794 (([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),

   795 (([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),

   796 (([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),

   797 (([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

   798  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),

   799 (([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),

   800 (([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),

   801 (([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),

   802 (([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),

   803 (([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),

   804 (([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),

   805 (([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),

   806 (([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),

   807 (([10,4,4], Res), c = L * q_0 / 2),

   808 (([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),

   809 (([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),

   810 (([10], Res), [c = L * q_0 / 2, c_2 = 0]),

   811 (([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),

   812 (([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),

   813 (([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),

   814 (([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),

   815 (([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),

   816 (([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),

   817 (([15,1], Res), y' x =

   818 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +

   819 c)]*)

   821 "----------- Bsp 7.27 autoCalculate ------------------------------";

   822 "----------- Bsp 7.27 autoCalculate ------------------------------";

   823 "----------- Bsp 7.27 autoCalculate ------------------------------";

   824  reset_states ();

   825  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

   826 	     "RandbedingungenBiegung [y 0 = 0, y L = 0]",

   827 	     "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

   828 	     "FunktionsVariable x"],

   829 	    ("Biegelinie",

   830 	     ["MomentBestimmte","Biegelinien"],

   831 	     ["IntegrierenUndKonstanteBestimmen"]))];

   832  moveActiveRoot 1;

   833  autoCalculate 1 CompleteCalcHead;

   835  fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);

   836 (*

   837 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;

   838 val it = true : bool

   839 *)

   840  autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);

   841  val ((pt,_),_) = get_calc 1;

   842  case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))

   843 	  | _ => error  "biegelinie.sml: Bsp 7.27 autoCalculate#4c";

   845  autoCalculate 1 CompleteCalc;

   846 val ((pt,p),_) = get_calc 1;

   847 if p = ([], Res) andalso length (children pt) = 23 andalso

   848 term2str (get_obj g_res pt (fst p)) =

   849 "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)"

   850 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";

   852  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

   853  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;

   854  show_pt pt;

   856 (*check all formulae for getTactic*)

   857  getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);

   858  getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);

   859  getTactic 1 ([6],Res) (* ---"---                      ["M_b 0 = 0"]*);

   860  getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);

   861  getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);

   862  getTactic 1 ([8],Res) (* ---"---                      ["M_b L = 0"]*);

   864 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";

   865 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";

   866 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";

   867 val fmz =

   868     ["Streckenlast q_0","FunktionsVariable x",

   869      "Funktionen [Q x = c + -1 * q_0 * x, \

   870      \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\

   871      \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\

   872      \ 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)]"];

   873 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],

   874 		     ["Biegelinien","ausBelastung"]);

   875 val p = e_pos'; val c = [];

   876 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   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 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 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()

   882 | _ => error "biegelinie.sml met2 b";

   884 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =   "q_ x = q_0";

   885 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";

   886 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =  "Q' x = - q_0";

   887 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()

   888 | _ => error "biegelinie.sml met2 c";

   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;

   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;

   896 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";

   897 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";

   898 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";

   899 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()

   900 | _ => error "biegelinie.sml met2 d";

   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;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; f2str f =

   907 		   "M_b x = Integral c + -1 * q_0 * x D x";

   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 		   "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 		   "- EI * y'' 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 		   "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";

   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;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; f2str f =

   921     "y' x = Integral 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 = Integral 1 / (-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 =\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; 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;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;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; f2str f =

   933 "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";

   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; 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;

   939 if f2str f =

   940    "[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)]"

   941 then case nxt of ("End_Proof'", End_Proof') => ()

   942   | _ => error "biegelinie.sml met2 e 1"

   943 else error "biegelinie.sml met2 e 2";

   945 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

   946 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

   947 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

   948 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",

   949 	   "substitution (M_b L = 0)",

   950 	   "equality equ_equ"];

   951 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],

   952 		     ["Equation","fromFunction"]);

   953 val p = e_pos'; val c = [];

   954 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   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;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   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;

   960 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

   961 			"M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";

   962 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

   963                         "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";

   964 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

   965 			"0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";

   966 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   967 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   968 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)

   969    f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"

   970 then case nxt of ("End_Proof'", End_Proof') => ()

   971   | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"

   972 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";

   973 *} ML {*

   974 *}

   976 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)

   977   ML_file "Knowledge/algein.sml"

   978   ML_file "Knowledge/diophanteq.sml"

   979   ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"

   980   ML_file "Knowledge/inssort.sml"

   981   ML_file "Knowledge/isac.sml"

   982   ML_file "Knowledge/build_thydata.sml"

   983   ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}

   984   ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}

   985   ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"

   986   ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"

   987   ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}

   989   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

   990   ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}

   991   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

   993 section {* history of tests *}

   994 text {*

   995   Systematic regression tests have been introduced to isac development in 2003.

   996   Sanity of the regression tests suffers from updates following Isabelle development,

   997   which mostly exceeded the resources available in isac's development.

   999   The survey below shall support to efficiently use the tests for isac

  1000   on different Isabelle versions. Conclusion in most cases will be:

  1002   !!! Use most recent tests or go back to the old notebook

  1003       with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

  1004 *}

  1007 subsection {* isac on Isabelle2015 *}

  1008 subsubsection {* Summary of development *}

  1009 text {*

  1010   * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).

  1011     This complicates Test_Isac, see "Prepare running tests" above.

  1012   * Remove TTY interface.

  1013   * Re-activate insertion sort.

  1014 *}

  1015 subsubsection {* State of tests: unchanged *}

  1016 subsubsection {* Changesets of begin and end *}

  1017 text {*

  1018   last changeset with Test_Isac 2f1b2854927a

  1019   first changeset with Test_Isac ???

  1020 *}

  1022 subsection {* isac on Isabelle2014 *}

  1023 subsubsection {* Summary of development *}

  1024 text {*

  1025   migration from "isabelle tty" --> libisabelle

  1026 *}

  1028 subsection {* isac on Isabelle2013-2 *}

  1029 subsubsection {* Summary of development *}

  1030 text {*

  1031   reactivated context_thy

  1032 *}

  1033 subsubsection {* State of tests *}

  1034 text {*

  1035   TODO

  1036 *}

  1037 subsubsection {* Changesets of begin and end *}

  1038 text {*

  1039   TODO

  1040   :

  1041   : isac on Isablle2013-2

  1042   :

  1043   Changeset: 55318 (03826ceb24da) merged

  1044   User: Walther Neuper <neuper@ist.tugraz.at>

  1045   Date: 2013-12-12 14:27:37 +0100 (7 minutes)

  1046 *}

  1048 subsection {* isac on Isabelle2013-1 *}

  1049 subsubsection {* Summary of development *}

  1050 text {*

  1051   Isabelle2013-1 was replaced within a few weeks due to problems with the document model;

  1052   no significant development steps for ISAC.

  1053 *}

  1054 subsubsection {* State of tests *}

  1055 text {*

  1056   See points in subsection "isac on Isabelle2011", "State of tests".

  1057 *}

  1058 subsubsection {* Changesets of begin and end *}

  1059 text {*

  1060   Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy

  1061   User: Walther Neuper <neuper@ist.tugraz.at>

  1062   Date: 2013-12-03 18:13:31 +0100 (8 days)

  1063   :

  1064   : isac on Isablle2013-1

  1065   :

  1066   Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect

  1067   User: Walther Neuper <neuper@ist.tugraz.at>

  1068   Date: 2013-11-21 18:12:17 +0100 (2 weeks)

  1070 *}

  1072 subsection {* isac on Isabelle2013 *}

  1073 subsubsection {* Summary of development *}

  1074 text {*

  1075   # Oct.13: replaced "axioms" by "axiomatization"

  1076   # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref

  1077   # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into

  1078     simplification of multivariate rationals (without improving the rulesets involved).

  1079 *}

  1080 subsubsection {* Run tests *}

  1081 text {*

  1082   Is standard now; this subsection will be discontinued under Isabelle2013-1

  1083 *}

  1084 subsubsection {* State of tests *}

  1085 text {*

  1086   See points in subsection "isac on Isabelle2011", "State of tests".

  1087   # re-activated listC.sml

  1088 *}

  1089 subsubsection {* Changesets of begin and end *}

  1090 text {*

  1091   changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"

  1092   User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>

  1093   Date: Tue Nov 19 22:23:30 2013 +0000

  1094   :

  1095   : isac on Isablle2013

  1096   :

  1097   Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013

  1098   User: Walther Neuper <neuper@ist.tugraz.at>

  1099   Date: 2013-07-15 08:28:50 +0200 (4 weeks)

  1100 *}

  1102 subsection {* isac on Isabelle2012 *}

  1103 subsubsection {* Summary of development *}

  1104 text {*

  1105   isac on Isabelle2012 is considered just a transitional stage

  1106   within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;

  1107   For considerations on the transition see

  1108   ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".

  1109 *}

  1110 subsubsection {* Run tests *}

  1111 text {*

  1112 $ cd /usr/local/isabisac12/

  1113 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy

  1114 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy

  1115 *}

  1116 subsubsection {* State of tests *}

  1117 text {*

  1118   At least the tests from isac on Isabelle2011 run again.

  1119   However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling

  1120   in parallel with evaluation.

  1122   Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)

  1123   yields 69 hits, some of which were already present before Isabelle2002-->2009-2

  1124   (i.e. on the old notebook from 2002).

  1126   Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:

  1127   # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy

  1128   # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002

  1129   # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002

  1130   Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.

  1132   Some tests have been re-activated (e.g. error patterns, fill patterns).

  1133 *}

  1134 subsubsection {* Changesets of begin and end *}

  1135 text {*

  1136   Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012

  1137   User: Walther Neuper <neuper@ist.tugraz.at>

  1138   Date: 2013-07-11 16:58:31 +0200 (4 weeks)

  1139   :

  1140   : isac on Isablle2012

  1141   :

  1142   Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012

  1143   User: Walther Neuper <neuper@ist.tugraz.at>

  1144   Date: 2012-09-24 18:35:13 +0200 (8 months)

  1145   ------------------------------------------------------------------------------

  1146   Changeset: 48756 (7443906996a8) merged

  1147   User: Walther Neuper <neuper@ist.tugraz.at>

  1148   Date: 2012-09-24 18:15:49 +0200 (8 months)

  1149 *}

  1151 subsection {* isac on Isabelle2011 *}

  1152 subsubsection {* Summary of development *}

  1153 text {*

  1154   isac's mathematics engine has been extended by two developments:

  1155   (1) Isabelle's contexts were introduced by Mathias Lehnfeld

  1156   (2) Z_Transform was introduced by Jan Rocnik, which revealed

  1157     further errors introduced by (1).

  1158   (3) "error patterns" were introduced by Gabriella Daroczy

  1159   Regressions tests have been added for all of these.

  1160 *}

  1161 subsubsection {* Run tests *}

  1162 text {*

  1163   $ cd /usr/local/isabisac11/

  1164   $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy

  1165   $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy

  1166 *}

  1167 subsubsection {* State of tests *}

  1168 text {*

  1169   Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)

  1170   and sometimes give reasons for failing tests.

  1171   (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable

  1172   work, some of which couldn't be revised (and renamed) by WN and thus survived some time.

  1174   The most signification tests (in particular Frontend/interface.sml) run,

  1175   however, many "error in kernel" are not caught by an exception.

  1176   ------------------------------------------------------------------------------

  1177   After the changeset below Test_Isac worked with check_unsynchronized_ref ():

  1178   ------------------------------------------------------------------------------

  1179   Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref

  1180   User: Walther Neuper <neuper@ist.tugraz.at>

  1181   Date: 2012-08-06 10:38:11 +0200 (11 months)

  1184   The list below records TODOs while producing an ISAC kernel for

  1185   gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING

  1186   (so to be resumed with Isabelle2013-1):

  1187   ############## WNxxxxxx.TODO can be found in sources ##############

  1188   --------------------------------------------------------------------------------

  1189   WN111013.TODO: lots of cleanup/removal in test/../Test.thy

  1190   --------------------------------------------------------------------------------

  1191   WN111013.TODO: remove concept around "fun init_form", lots of troubles with

  1192   this special case (see) --- why not nxt = Model_Problem here ? ---

  1193   --------------------------------------------------------------------------------

  1194   WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/

  1195   ... FIRST redesign

  1196   # simplify_* , *_simp_*

  1197   # norm_*

  1198   # calc_* , calculate_*  ... require iteration over all rls ...

  1199   ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !

  1200   --------------------------------------------------------------------------------

  1201   WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!

  1202   --------------------------------------------------------------------------------

  1203   WN120314 changeset a393bb9f5e9f drops root equations.

  1204   see test/Tools/isac/Knowledge/rootrateq.sml

  1205   --------------------------------------------------------------------------------

  1206   WN120317.TODO changeset 977788dfed26 dropped rateq:

  1207   # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002

  1208   # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:

  1209     investigation Check_elementwise stopped due to too much effort finding out,

  1210     why Check_elementwise worked in 2002 in spite of the error.

  1211   --------------------------------------------------------------------------------

  1212   WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl

  1213   --------------------------------------------------------------------------------

  1214   WN120317.TODO found by test --- interSteps for Schalk 299a --- that

  1215     NO test with 'interSteps' is checked properly (with exn on changed behaviour)

  1216   --------------------------------------------------------------------------------

  1217   WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has

  1218     a newly outcommented test where rewrite_set_ make_polynomial --> NONE

  1219   --------------------------------------------------------------------------------

  1220   WN120320.TODO check-improve rlsthmsNOTisac:

  1221   DONE make test --- old compute rlsthmsNOTisac by eq_thmI'

  1222   DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy

  1223   FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab

  1224   # mark twice thms (in isac + (later) in Isabelle) in Isac.thy

  1225   --------------------------------------------------------------------------------

  1226   WN120320.TODO rlsthmsNOTisac: replace twice thms ^

  1227   --------------------------------------------------------------------------------

  1228   WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test

  1229   --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.

  1230   --------------------------------------------------------------------------------

  1231   WN120321.TODO rearrange theories:

  1232     Knowledge

  1233       :

  1234       Atools.thy

  1235       ///Descript.thy --> ProgLang

  1236       Delete.thy   <--- first_Knowledge_thy (*mv to Atools.thy*)

  1237     ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy

  1238           Interpret.thy are generated (simplifies xml structure for theories)

  1239       Script.thy

  1240       Tools.thy

  1241       ListC.thy    <--- first_Proglang_thy

  1242   --------------------------------------------------------------------------------

  1243   WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify

  1244       EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"

  1245   broken during work on thy-hierarchy

  1246   --------------------------------------------------------------------------------

  1247   WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see

  1248   test --- the_hier (get_thes ()) (collect_thydata ())---

  1249   --------------------------------------------------------------------------------

  1250   WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_

  1251   !!add mutual crossreferences to ?fun headline??? where the same has to be done:

  1252   !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!

  1253   --------------------------------------------------------------------------------

  1254   WN120409.TODO replace "op mem" (2002) with member (2011) ...

  1255   ... an exercise interesting for beginners !

  1256   --------------------------------------------------------------------------------

  1257   WN120411 scanning html representation of newly generated knowledge:

  1258   * thy:

  1259   ** Theorems: only "Proof of the theorem" (correct!)

  1260                and "(c) isac-team (math-autor)"

  1261   ** Rulesets: only "Identifier:///"

  1262                and "(c) isac-team (math-autor)"

  1263   ** IsacKnowledge: link to dependency graph (which needs to be created first)

  1264   ** IsacScripts --> ProgramLanguage

  1265   *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen

  1267   * pbl: OK !?!

  1268   * met: OK !?!

  1269   * exp:

  1270   ** Z-Transform is missing !!!

  1271   ** type-constraints !!!

  1272   --------------------------------------------------------------------------------

  1273   WN120417: merging xmldata revealed:

  1274   ..............NEWLY generated:........................................

  1275   <THEOREMDATA>

  1276     <GUH> thy_isab_Fun-thm-o_apply </GUH>

  1277     <STRINGLIST>

  1278       <STRING> Isabelle </STRING>

  1279       <STRING> Fun </STRING>

  1280       <STRING> Theorems </STRING>

  1281       <STRING> o_apply </STRING>

  1282     </STRINGLIST>

  1283       <MATHML>

  1284         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>

  1285       </MATHML>  <PROOF>

  1286       <EXTREF>

  1287         <TEXT> Proof of the theorem </TEXT>

  1288         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>

  1289       </EXTREF>

  1290     </PROOF>

  1291     <EXPLANATIONS> </EXPLANATIONS>

  1292     <MATHAUTHORS>

  1293       <STRING> Isabelle team, TU Munich </STRING>

  1294     </MATHAUTHORS>

  1295     <COURSEDESIGNS>

  1296     </COURSEDESIGNS>

  1297   </THEOREMDATA>

  1298   ..............OLD FORMAT:.............................................

  1299   <THEOREMDATA>

  1300     <GUH> thy_isab_Fun-thm-o_apply </GUH>

  1301     <STRINGLIST>

  1302       <STRING> Isabelle </STRING>

  1303       <STRING> Fun </STRING>

  1304       <STRING> Theorems </STRING>

  1305       <STRING> o_apply </STRING>

  1306     </STRINGLIST>

  1307     <THEOREM>

  1308       <ID> o_apply </ID>

  1309       <MATHML>

  1310         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>

  1311       </MATHML>

  1312     </THEOREM>

  1313     <PROOF>

  1314       <EXTREF>

  1315         <TEXT> Proof of the theorem </TEXT>

  1316         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>

  1317       </EXTREF>

  1318     </PROOF>

  1319     <EXPLANATIONS> </EXPLANATIONS>

  1320     <MATHAUTHORS>

  1321       <STRING> Isabelle team, TU Munich </STRING>

  1322     </MATHAUTHORS>

  1323     <COURSEDESIGNS>

  1324     </COURSEDESIGNS>

  1325   </THEOREMDATA>

  1326   --------------------------------------------------------------------------------

  1327 *}

  1328 subsubsection {* Changesets of begin and end *}

  1329 text {*

  1330   isac development was done between these changesets:

  1331   ------------------------------------------------------------------------------

  1332   Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files

  1333   User: Walther Neuper <neuper@ist.tugraz.at>

  1334   Date: 2012-09-24 16:39:30 +0200 (8 months)

  1335   :

  1336   : isac on Isablle2011

  1337   :

  1338   Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011

  1339   Branch: decompose-isar

  1340   User: Walther Neuper <neuper@ist.tugraz.at>

  1341   Date: 2011-02-25 13:04:56 +0100 (2011-02-25)

  1342   ------------------------------------------------------------------------------

  1343 *}

  1345 subsection {* isac on Isabelle2009-2 *}

  1346 subsubsection {* Summary of development *}

  1347 text {*

  1348   In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.

  1349   The update was painful (bridging 7 years of Isabelle development) and cut short

  1350   due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and

  1351   going on to Isabelle2011 although most of the tests did not run.

  1352 *}

  1353 subsubsection {* Run tests *}

  1354 text {*

  1355   WN131021 this is broken by installation of Isabelle2011/12/13,

  1356   because all these write their binaries to ~/.isabelle/heaps/..

  1358   $ cd /usr/local/isabisac09-2/

  1359   $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy

  1360   $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy

  1361   NOT THE RIGHT VERSION.....    test/Tools/isac/Test_Isac.thy !!!

  1362 *}

  1363 subsubsection {* State of tests *}

  1364 text {*

  1365   Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.

  1366 *}

  1367 subsubsection {* Changesets of begin and end *}

  1368 text {*

  1369   isac development was done between these changesets:

  1370   ------------------------------------------------------------------------------

  1371   Changeset: 38115 (940a5feea094) Little improvements of isac-plugin

  1372   Branch: decompose-isar

  1373   User: Marco Steger <m.steger@student.tugraz.at>

  1374   Date: 2011-02-06 18:30:28 +0100 (2011-02-06)

  1375   :

  1376   : isac on Isablle2009-2

  1377   :

  1378   Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2

  1379   Branch: isac-from-Isabelle2009-2

  1380   User: Walther Neuper <neuper@ist.tugraz.at>

  1381   Date: 2010-07-21 09:59:35 +0200 (2010-07-21)

  1382   ------------------------------------------------------------------------------

  1383 *}

  1385 subsection {* isac on Isabelle2002 *}

  1386 subsubsection {* Summary of development *}

  1387 text {*

  1388   From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")

  1389   of isac's mathematics engine has been implemented.

  1390 *}

  1391 subsubsection {* Run tests *}

  1392 subsubsection {* State of tests *}

  1393 text {*

  1394   All tests work on an old notebook (the right PolyML coudn't be upgraded to more

  1395   recent Linux versions)

  1396 *}

  1397 subsubsection {* Changesets of begin and end *}

  1398 text {*

  1399   Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;

  1400   see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.

  1401 *}

  1403 end

  1404 (*========== inhibit exn 130719 Isabelle2013 ===================================

  1405 ============ inhibit exn 130719 Isabelle2013 =================================*)

  1407 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

  1408   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 08 Mar 2018 07:28:17 +0100
changeset 59395	862eb17f9e16
parent 59388	47877d6fa35a
child 59396	d1aae4e79859
permissions	-rwxr-xr-x