(* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)

   Author: Walther Neuper 101001

   (c) copyright due to license terms.

   Isac's tests are organised parallel to sources: 

     "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"

   plus

     ~~/test/Tools/isac/ADDTESTS

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

-------------------------------------------------------------------------------

Prepare running tests: see below

Run tests:

$ cd /usr/local/isabisac/

$ export ISABELLE_VERSION=2015 # for libisabelle

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

*)

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

text \<open>

Isac encapsulates code as much as possible in structures without open. TODO ProgLang.

This policy conflicts with those tests, which go into functions to details

not declared in the signatures.

In order to maintain these tests without changes, this has to be done before running tests:

(1) Extend signatures for tests by

    ~~$ ./xcoding-to-test.sh

    ~~$ ./zcoding-to-test.sh  # -"- + go back to Test_Isac.thy

    Running Test_Isac.thy opens all structures, see code after "begin" below.

(2) Clean signatures for coding

    ~~$ ./xtest-to-coding.sh

    ~~$ ./xtest-to-coding.sh  # -"- + go back to coding (!update thy!)

********************* don't forget (2) BEFORE pushing to repository *********************

The above bash files accomplish query replace in src/Tools/isac:

    \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>

    \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit>   \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>

     ^^^ in signature outcommented,                     ^^^ NOT outcommented,

         this is status for coding                          this is status for tests

\<close>

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

text \<open>

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

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

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

\<close>

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

text \<open>

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

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

\<close>

theory Test_Isac imports Build_Thydata

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

  "ADDTESTS/accumulate-val/Thy_All"

  "ADDTESTS/Ctxt"

  "ADDTESTS/test-depend/Build_Test"

  "ADDTESTS/All_Ctxt"

  "ADDTESTS/Test_Units"

  "ADDTESTS/course/phst11/T1_Basics"

  "ADDTESTS/course/phst11/T2_Rewriting"

  "ADDTESTS/course/phst11/T3_MathEngine"

  "ADDTESTS/file-depend/BuildC_Test"

  "ADDTESTS/session-get_theory/Foo"

(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"

   ADDTESTS/------------------------------------------- see end of tests *)

(*"~~/test/Pure/Isar/Test_Parsers"           dropped Isabelle2014-->2015 *)

(*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)

  "~~/test/Pure/Isar/Test_Parse_Term"

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

  "~~/test/Tools/isac/Interpret/ptyps"       (* setup for ptyps.sml    *)

  "~~/test/Tools/isac/ProgLang/calculate"    (* setup for calculate.sml*)

  "~~/test/Tools/isac/ProgLang/scrtools"     (* setup for scrtools.sml *)

  "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)

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

  "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)

  "~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)

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

begin

ML {*

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)

                      (* these vvv test, if funs are intermediately opened in structure 

                         in case of errors here consider ~~/./xtest-to-coding.sh      *)

  open Kernel;

  open Math_Engine;            CalcTreeTEST;

  open Lucin;                  appy;

  open Inform;                 cas_input;

  open Rtools;                 trtas2str;

  open Chead;                  pt_extract;

  open Generate;               (* NONE *)

  open Ctree;                  append_problem;

  open Specify;                show_ptyps;

  open Applicable;             mk_set;

  open Solve;                  (* NONE *)

  open Selem;                  e_fmz;

  open Stool;                  transfer_asms_from_to;

  open Tac;                    (* NONE *)

  open Model;                  (* NONE *)

  open LTool;                  rule2stac;

  open Rewrite;                mk_thm;

  open Calc;                   get_pair;

  open TermC;                  ;

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

*}

ML {*

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

*} ML {*

*} ML {*

*}

ML {*

  KEStore_Elems.set_ref_thy @{theory};

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

*}

(*---------------------- check test file by testfile -------------------------------------------

  ---------------------- check test file by testfile -------------------------------------------*)

section {* trials with Isabelle's functions *}

  ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}

  ML_file "~~/test/Pure/General/alist.ML"

  ML_file "~~/test/Pure/General/basics.ML"

  ML_file "~~/test/Pure/General/scan.ML"

  ML_file "~~/test/Pure/PIDE/xml.ML"

  ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}

section {* test ML Code of isac *}

  ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}

  ML_file          "library.sml"

  ML_file          "calcelems.sml"

(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

  ML_file          "kestore.sml"        (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)

  ML_file "ProgLang/termC.sml"

  ML_file "ProgLang/calculate.sml"      (* requires setup from calculate.thy                    *)

  ML_file "ProgLang/rewrite.sml"

  ML_file "ProgLang/listC.sml"

  ML_file "ProgLang/scrtools.sml"

  ML_file "ProgLang/tools.sml"

(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

  ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}

  ML_file "Minisubpbl/000-comments.sml"

  ML_file "Minisubpbl/100-init-rootpbl.sml"

  ML_file "Minisubpbl/150-add-given.sml"

  ML_file "Minisubpbl/200-start-method.sml"

  ML_file "Minisubpbl/300-init-subpbl.sml"

  ML_file "Minisubpbl/400-start-meth-subpbl.sml"

  ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"

  ML_file "Minisubpbl/500-met-sub-to-root.sml"

  ML_file "Minisubpbl/530-error-Check_Elementwise.sml"

  ML_file "Minisubpbl/600-postcond.sml"

  ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}

  ML_file "Interpret/mstools.sml"

  ML_file "Interpret/ctree.sml"         (*!...!see(25)*)

  ML_file "Interpret/ptyps.sml"         (* requires setup from ptyps.thy *)

  ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}

(*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)

  ML_file "Interpret/generate.sml"

(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

  ML_file "Interpret/calchead.sml"

  ML_file "Interpret/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)

  ML_file "Interpret/rewtools.sml"

  ML_file "Interpret/script.sml"

  ML_file "Interpret/solve.sml"

  ML_file "Interpret/inform.sml"

(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

  ML_file "Interpret/mathengine.sml"    (*!part. WN130804: +check Interpret/me.sml*)

ML {*

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

reset_states ();

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

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

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

Iterator 1;

moveActiveRoot 1;

(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

modeling is skipped FIXME 

see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:

 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "Test");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

autoCalculate 1 (Step 1); 

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

autoCalculate 1 (Step 1);

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

autoCalculate 1 (Step 1);

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

autoCalculate 1 (Step 1);

*} ML {*

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

autoCalculate 1 (Step 1);

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

*} ML {*

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

*} ML {*

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

autoCalculate 1 (Step 1);

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

*} ML {*

term2str t;

*} ML {*

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

autoCalculate 1 (Step 1);

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

*} ML {*

term2str t;

*} ML {*

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

autoCalculate 1 (Step 1);

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

*} ML {*

term2str t;

*} ML {*

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

autoCalculate 1 (Step 1);

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

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

*} ML {*

*} ML {*

term2str t

*} ML {*

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

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

*} ML {*

*} ML {*

*}

  ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}

  ML_file "xmlsrc/mathml.sml"           (*part.*)

  ML_file "xmlsrc/datatypes.sml"        (*TODO/part.*)

  ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)

  ML_file "xmlsrc/thy-hierarchy.sml"

  ML_file "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)

  ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}

  ML_file "Frontend/messages.sml"

  ML_file "Frontend/states.sml"

  ML_file "Frontend/interface.sml"

  ML_file "Frontend/use-cases.sml"

(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

  ML_file          "print_exn_G.sml"

  ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}

  ML_file "Knowledge/delete.sml"

  ML_file "Knowledge/descript.sml"

  ML_file "Knowledge/atools.sml"

  ML_file "Knowledge/simplify.sml"

  ML_file "Knowledge/poly.sml"

  ML_file "Knowledge/gcd_poly_ml.sml"

  ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)

  ML_file "Knowledge/rational.sml"

  ML_file "Knowledge/equation.sml"

  ML_file "Knowledge/root.sml"

  ML_file "Knowledge/lineq.sml"

(*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)

  ML_file "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)

  ML_file "Knowledge/rootrat.sml"

  ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)

  ML_file "Knowledge/partial_fractions.sml"

  ML_file "Knowledge/polyeq.sml"

(*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)

  ML_file "Knowledge/calculus.sml"

  ML_file "Knowledge/trig.sml"

(*ML_file "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 

  ML_file "Knowledge/diff.sml"

  ML_file "Knowledge/integrate.sml"

ML {*

*} ML {*

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

val thy = @{theory "Isac"};

"===== test 1";

val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

"----- stepwise from the rulesets in simplify_Integral and below-----";

val rls = norm_Rational_noadd_fractions;

case rewrite_set_inst_ thy true subs rls t of

    SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"

  | NONE => ();

"===== test 2";

val rls = order_add_mult_in;

val SOME (t,[]) = rewrite_set_ thy true rls t;

if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()

else error "integrate.sml simplify by ruleset order_add_mult_in #2";

"===== test 3";

val rls = discard_parentheses;

val SOME (t,[]) = rewrite_set_ thy true rls t;

if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()

else error "integrate.sml simplify by ruleset discard_parenth.. #3";

"===== test 4";

val rls = 

  (append_rls "separate_bdv" collect_bdv

 	  [Thm ("separate_bdv", num_str @{thm separate_bdv}),

 		  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

 		 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),

      (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)

 		Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),

 		  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)

 		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})

       (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

    ]);

(*show_types := true;  --- do we need type-constraint in thms? *)

@{thm separate_bdv};     (*::?'a does NOT rewrite here WITHOUT type constraint*)

@{thm separate_bdv_n};   (*::real ..because of ^^^, rewrites*)

@{thm separate_1_bdv};   (*::?'a*)

val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)

@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)

(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)

val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;

if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

else error "integrate.sml simplify by ruleset separate_bdv.. #4";

"===== test 5";

val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

val rls = simplify_Integral;

val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

(* given was:   "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)

if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

else error "integrate.sml, simplify_Integral #99";

"........... 2nd integral ........................................";

"........... 2nd integral ........................................";

"........... 2nd integral ........................................";

val t = str2t 

"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";

val rls = simplify_Integral;

val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

if term2str t =

   "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"

then () else raise error "integrate.sml, simplify_Integral #198";

val rls = integration_rules;

val SOME (t,[]) = rewrite_set_ thy true rls t;

term2str t;

if term2str t = 

   "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"

then () else error "integrate.sml, simplify_Integral #199";

"----------- integrate by ruleset -----------------------";*} ML {*

*}

  ML_file "Knowledge/eqsystem.sml"

  ML_file "Knowledge/test.sml"

  ML_file "Knowledge/polyminus.sml"

  ML_file "Knowledge/vect.sml"

  ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)

  ML_file "Knowledge/biegelinie-1.sml"

ML {*

*} ML {*

(* tests on biegelinie

   author: Walther Neuper 050826

   (c) due to copyright terms

*)

*} ML {*

trace_rewrite := false;

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- the rules -------------------------------------------";

"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";

"----------- simplify_leaf for this script -----------------------";

"----------- Bsp 7.27 me -----------------------------------------";

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

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

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

"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";

"----------- investigate normalforms in biegelinien --------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

val thy = @{theory "Biegelinie"};

val ctxt = thy2ctxt' "Biegelinie";

fun str2term str = (Thm.term_of o the o (parse thy)) str;

fun term2s t = term_to_string'' "Biegelinie" t;

fun rewrit thm str = 

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

*} ML {*

"----------- the rules -------------------------------------------";

"----------- the rules -------------------------------------------";

"----------- the rules -------------------------------------------";

val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;

if term2s t = "Q' x = - q_0" then ()

else error  "/biegelinie.sml: Belastung_Querkraft";

val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;

if term2s t = "M_b' x = - q_0 * x + c" then ()

else error  "/biegelinie.sml: Querkraft_Moment";

val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");

    term2s t;

if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()

else error  "biegelinie.sml: Moment_Neigung";

*} ML {*

"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";

"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";

"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";

"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";

val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";

val t = rewrit @{thm Moment_Neigung} t;

if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()

else error "Moment_Neigung broken";

(* was       I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"

   before declaring "y''" as a constant *)

val t = rewrit @{thm make_fun_explicit} t; 

if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()

else error "make_fun_explicit broken";

*} ML {*

"----------- simplify_leaf for this script -----------------------";

"----------- simplify_leaf for this script -----------------------";

"----------- simplify_leaf for this script -----------------------";

val srls = Rls {id="srls_IntegrierenUnd..", 

		preconds = [], 

		rew_ord = ("termlessI",termlessI), 

		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

				  [(*for asm in NTH_CONS ...*)

				   Calc ("Orderings.ord_class.less",eval_equ "#less_"),

				   (*2nd NTH_CONS pushes n+-1 into asms*)

				   Calc("Groups.plus_class.plus", eval_binop "#add_")

				   ], 

		srls = Erls, calc = [], errpatts = [],

		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),

			 Calc("Groups.plus_class.plus", eval_binop "#add_"),

			 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

			 Calc("Tools.lhs", eval_lhs "eval_lhs_"),

			 Calc("Tools.rhs", eval_rhs "eval_rhs_"),

			 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")

			 ],

		scr = EmptyScr};

val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";

val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";

val SOME (e1__,_) = rewrite_set_ thy false srls 

  (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);

if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";

val SOME (x1__,_) = 

    rewrite_set_ thy false srls 

		 (str2term"argument_in (lhs (M_b 0 = 0))");

if term2str x1__ = "0" then ()

else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";

(*trace_rewrite := true; ..stopped Test_Isac.thy*)

trace_rewrite:=false;

*} ML {*

"----------- Bsp 7.27 me -----------------------------------------";

"----------- Bsp 7.27 me -----------------------------------------";

"----------- Bsp 7.27 me -----------------------------------------";

val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

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

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

	   "FunktionsVariable x"];

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

  ("Biegelinie",["MomentBestimmte","Biegelinien"],

   ["IntegrierenUndKonstanteBestimmen"]);

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

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

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

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

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

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

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

*} ML {*

val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);

(*if itms2str_ ctxt pits = ... all 5 model-items*)

val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);

if itms2str_ ctxt mits = "[]" then ()

else error  "biegelinie.sml: Bsp 7.27 #2";

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

case nxt of (_,Add_Given "FunktionsVariable x") => ()

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

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

val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);

(*if itms2str_ ctxt mits = ... all 6 guard-items*)

case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()

	  | _ => error  "biegelinie.sml: Bsp 7.27 #4b";

"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";

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

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

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

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

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

*} ML {*

case nxt of 

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

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

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

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

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

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

case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()

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

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

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

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

case nxt of 

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

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

*} ML {*

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

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

case nxt of 

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

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

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

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

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

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

case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()

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

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

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);

f2str f;

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

case nxt of (_, Substitute ["x = 0"]) => ()

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

*} ML {*

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

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

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

else error  "biegelinie.sml: Bsp 7.27 #8";

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

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

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

*} ML {*

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

else error  "biegelinie.sml: Bsp 7.27 #9";

*} ML {*

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

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

*} ML {*

nxt;

*} ML {*

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

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

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

    val (pt, p) = ptp;

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

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

val pIopt = get_pblID (pt,ip);

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

tacis = [];

pIopt (*SOME*);

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

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

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

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

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

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

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

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

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

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

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

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

  	    val (_, tac) =

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

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

*} ML {*

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

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

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

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

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

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

*} ML {*

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

*} ML {*

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

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

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

*} ML {*

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

*} ML {*

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

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

*} ML {*

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

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

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

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

*} ML {*

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

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

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

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

(*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()

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

*} ML {*

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

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

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

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

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

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

case nxt of

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

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

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

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

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

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

case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()

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

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

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

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

case nxt of

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

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

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

if f2str f =

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

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

case nxt of

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

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

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

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

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

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

case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()

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

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

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

if f2str f = 

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

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

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

case nxt of

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

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

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

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

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

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

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

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

case nxt of

    (_, Subproblem

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

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

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

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

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

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

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

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

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

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

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

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

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

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

if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()

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

case nxt of

    (_, Subproblem

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()

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

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

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

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

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

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

if f2str f = 

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

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

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

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

show_pt pt;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

c)]*)

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

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

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

 reset_states ();

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

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

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

	     "FunktionsVariable x"],

	    ("Biegelinie",

	     ["MomentBestimmte","Biegelinien"],

	     ["IntegrierenUndKonstanteBestimmen"]))];

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead; 

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

(*

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

val it = true : bool

*)

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

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

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

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

 autoCalculate 1 CompleteCalc;  

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

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

term2str (get_obj g_res pt (fst p)) = 

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

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

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

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

 show_pt pt;

(*check all formulae for getTactic*)

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

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

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

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

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

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

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

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

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

val fmz = 

    ["Streckenlast q_0","FunktionsVariable x",

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

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

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

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

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

		     ["Biegelinien","ausBelastung"]);

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

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

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

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

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

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

case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

		   "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";

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

		   "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";

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

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

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

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

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

    "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";

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

"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";

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

"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";

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

"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";

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

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

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

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

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

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

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

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

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

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

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

if f2str f =

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

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

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

else error "biegelinie.sml met2 e 2";

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

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

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

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

	   "substitution (M_b L = 0)", 

	   "equality equ_equ"];

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

		     ["Equation","fromFunction"]);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*} ML {*

*}

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

  ML_file "Knowledge/algein.sml"

  ML_file "Knowledge/diophanteq.sml"

  ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"

  ML_file "Knowledge/inssort.sml"

  ML_file "Knowledge/isac.sml"

  ML_file "Knowledge/build_thydata.sml"

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

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

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

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

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

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

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

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

section {* history of tests *}