wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              Test_Code.init_calc @{context};

    10   open LItool;                 arguments_from_model;

    11   open Sub_Problem;

    12   open Fetch_Tacs;

    13   open Step

    14   open Env;

    15   open LI;                     scan_dn;

    16   open Istate;

    17   open Error_Pattern;

    18   open Error_Pattern_Def;

    19   open Specification;

    20   open Ctree;                  append_problem;

    21   open Pos;

    22   open Program;

    23   open Prog_Tac;

    24   open Tactical;

    25   open Prog_Expr;

    26   open Auto_Prog;              rule2stac;

    27   open Input_Descript;

    28   open Specify;

    29   open Specify;

    30   open Step_Specify;

    31   open Step_Solve;

    32   open Step;

    33   open Solve;                  (* NONE *)

    34   open ContextC;               transfer_asms_from_to;

    35   open Tactic;                 (* NONE *)

    36   open I_Model;

    37   open O_Model;

    38   open P_Model;                (* NONE *)

    39   open Rewrite;

    40   open Eval;                   get_pair;

    41   open TermC;

    42   open Rule;

    43   open Rule_Set;               Sequence;

    44   open Eval_Def

    45   open ThyC

    46   open ThmC_Def

    47   open ThmC

    48   open Rewrite_Ord

    49   open UnparseC;

    51   Know_Store.set_ref_last_thy @{theory};

    52   (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)

    53 \<close>

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

    56 ML \<open>

    57 \<close> ML \<open>

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

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

    60 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    61 "~~~~~ continue fun xxx"; val () = ();

    62 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

    63 "xx"

    64 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

    65 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

    66 (*//------------------ adhoc inserted n ----------------------------------------------------\\*)

    67 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

    68 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

    70 val return_XXXXX = "XXXXX"

    71 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

    72 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

    73 \<close> ML \<open> (*||----------- continuing XXXXX ------------------------------------------------------*)

    74 (*||------------------ continuing XXXXX ------------------------------------------------------*)

    75 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

    76 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

    77 val "XXXXX" = return_XXXXX;

    79 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

    80 (*//------------------ inserted hidden code ------------------------------------------------\\*)

    81 (*\\------------------ inserted hidden code ------------------------------------------------//*)

    82 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

    84 \<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)

    85 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)

    86 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)

    87 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)

    88 \<close>

    89 ML \<open>

    90 \<close> ML \<open>

    91 \<close> ML \<open>

    92 \<close>

    93 text \<open>

    94   declare [[show_types]]

    95   declare [[show_sorts]]

    96   find_theorems "?a <= ?a"

    98   print_theorems

    99   print_facts

   100   print_statement ""

   101   print_theory

   102   ML_command \<open>Pretty.writeln prt\<close>

   103   declare [[ML_print_depth = 999]]

   104   declare [[ML_exception_trace]]

   105 \<close>

   107 section \<open>===================================================================================\<close>

   108 section \<open>=====  ============================================================================\<close>

   109 ML \<open>

   110 \<close> ML \<open>

   112 \<close> ML \<open>

   113 \<close>

   115 section \<open>===================================================================================\<close>

   116 section \<open>===== biegelinie-2.sml ============================================================\<close>

   117 ML \<open>

   118 \<close> ML \<open>

   119 (* Title:  Knowledge/biegelinie-2.sml

   120    author: Walther Neuper 190515

   121    (c) due to copyright terms

   122 *)

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

   124 "-----------------------------------------------------------------";

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

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

   127 "-----------------------------------------------------------------";

   128 "-----------------------------------------------------------------";

   129 "-----------------------------------------------------------------";

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

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

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

   135 val fmz =

   136     ["Streckenlast q_0", "FunktionsVariable x",

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

   138      \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\

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

   140      \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",

   141     "AbleitungBiegelinie dy"];

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

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

   145 States.reset ();

   146 CalcTree @{context} [(fmz, (dI',pI',mI'))];

   147 Iterator 1;

   148 moveActiveRoot 1;

   149 autoCalculate 1 CompleteCalc;

   151 val ((pt, p),_) = States.get_calc 1;

   152 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",

   153    UNDETECTED BY Test_Isac_Short.thy ===========================================================\\

   154 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term @{context}) =

   155    "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

   156 then () else error "auto SubProblem (_,[vonBelastungZu,Biegelinien] changed";

   157 ===============================================================================================//*)

   160 \<close> ML \<open>

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

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

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

   164 val fmz =

   165     ["Streckenlast q_0", "FunktionsVariable x",

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

   167      \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\

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

   169      \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",

   170     "AbleitungBiegelinie dy"];

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

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

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

   174 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt

   175 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt

   176 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt

   177 \<close> ML \<open> (*isa*)

   178 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt

   179 \<close> text \<open> (*isa2* )

   180 (*/---broken elementwise input to lists---\*)

   181 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen [Q x = c + - 1 * q_0 * x]" = nxt

   182 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt

   183 ( *\---broken elementwise input to lists---/*)

   184 \<close> ML \<open>

   185 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt

   186 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["vonBelastungZu", "Biegelinien"] = nxt

   187 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "ausBelastung"] = nxt

   188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt

   189 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   190 val return_me_Add_Given_AbleitungBiegelinie

   191                      = me nxt p c pt;

   192 \<close> ML \<open> (*//----------- step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)

   193 (*//------------------ step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)

   194 \<close> ML \<open>

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

   196 \<close> ML \<open>

   197       val ctxt = Ctree.get_ctxt pt p

   198       val (pt, p) =

   199   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   200   	    case Step.by_tactic tac (pt, p) of

   201   		    ("ok", (_, _, ptp)) => ptp

   202 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   203     (*case*)

   204       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

   205 \<close> ML \<open>

   206 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =

   207   (p, ((pt, Pos.e_pos'), []));

   208 \<close> ML \<open>

   209   (*if*) Pos.on_calc_end ip (*else*);

   210 \<close> ML \<open>

   211       val (_, probl_id, _) = Calc.references (pt, p);

   212 \<close> ML \<open>

   213 val _ =

   214       (*case*) tacis (*of*);

   215 \<close> ML \<open>

   216         (*if*) probl_id = Problem.id_empty (*else*);

   217 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   218            switch_specify_solve p_ (pt, ip);

   219 \<close> ML \<open>

   220 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

   221 \<close> ML \<open>

   222       (*if*) Pos.on_specification ([], state_pos) (*then*);

   223 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   224            specify_do_next (pt, input_pos);

   225 \<close> ML \<open>

   226 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

   227 \<close> ML \<open>

   228     val (_, (p_', tac)) = Specify.find_next_step ptp

   229     val ist_ctxt =  Ctree.get_loc pt (p, p_)

   230 \<close> ML \<open>

   231 val Tactic.Apply_Method mI =

   232     (*case*) tac (*of*);

   233 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   234   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

   235   	      ist_ctxt (pt, (p, p_'));

   236 \<close> ML \<open>

   237 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =

   238   ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

   239 \<close> ML \<open>

   240       val (itms, oris, probl) = case get_obj I pt p of

   241           PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

   242         | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

   243       val {model, ...} = MethodC.from_store ctxt mI;

   244 \<close> ML \<open>

   245 (*+*)val "Biegelinien/ausBelastung" = mI |> References.implode_id

   246 \<close> ML \<open>

   247 (*+* ===== current MethodC i_model ==============================================================*)

   248 (*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^

   249   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   250   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   251   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^

   252 (*  ...................... Cor Biegemoment M_b,

   253     ...................... Cor Querkraft Q    , *)

   254   "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"

   255 (* ...................... Cor Biegelinie y    , *)

   256 then () else error "by_tactic: parent "

   257 \<close> ML \<open>

   258 (*+* ===== current o_model created from Formalise.model of SubProblem ===========================*)

   259 (*+*)(oris |> O_Model.to_string @{context}) = "[\n" ^

   260   "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

   261   "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

   262   "(3, [\"1\"], #Find, Funktionen, [\"[Q x = c + - 1 * q_0 * x]\", \"[M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2]\", \"[y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)]\", \"[y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]\"]), \n" ^

   263   "(4, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

   264 \<close> ML \<open>

   265 (*+* ===== parent Problem i_model ===============================================================*)

   266 (*+*)(probl |> I_Model.to_string @{context}) = "[\n" ^

   267   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   268   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   269   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]))]"

   270 \<close> ML \<open>

   271       val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

   272 \<close> ML \<open>

   273 (*+* ===== current MethodC i_model complete'd ===================================================*)

   274 (*+*)(itms |> I_Model.to_string @{context}) = "[\n" ^

   275   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   276   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   277   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^

   278   "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"

   279 \<close> ML \<open>

   280 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   281       val (is, env, ctxt, prog) = case

   282     LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of

   283           (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)

   284 \<close> ML \<open>

   285 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);

   286 \<close> ML \<open>

   287     val (model_patt, program, prog, prog_rls, where_, where_rls) =

   288       case MethodC.from_store ctxt met_id of

   289         {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>

   290           (model_patt, program, prog, prog_rls, where_, where_rls)

   291 \<close> ML \<open>

   292 (*+* ===== MethodC model_patt ===================================================================*)

   293 (*+*)if (model_patt |> Model_Pattern.to_string @{context}) = "[\"" ^

   294   (*5 elements ------------------------------------------ ERROR:  -------------CORRECT:          *)

   295   "(#Given, (Streckenlast, q__q))\", \"" ^

   296   "(#Given, (FunktionsVariable, v_v))\", \"" ^

   297   "(#Given, (Biegelinie, b_b))\", \"" ^             (*\<longrightarrow> (b_b, dy)            (b_b, y)          *)

   298   "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*\<longrightarrow> (id_der, [Q x =..])  (id_der, dy)      *)

   299   "(#Find, (Funktionen, fun_s))\"]"                 (*                         (fun_s, [Q x =..])*)

   300 then () else error "init_pstate initial model_patt CHANGED"

   301 \<close> ML \<open>

   302 (*+*)if (i_model |> I_Model.to_string_TEST @{context}) = "[\n" ^

   303   "(1, [1], true ,#Given, (Cor_TEST Streckenlast q_0 , pen2str, Position.T)), \n" ^

   304   "(2, [1], true ,#Given, (Cor_TEST FunktionsVariable x , pen2str, Position.T)), \n" ^

   305   "(3, [1], true ,#Find, (Cor_TEST Funktionen\n [" ^

   306     "Q x = c + - 1 * q_0 * x, " ^

   307     "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  " ^

   308     "y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  " ^

   309     "y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] , pen2str, Position.T)), \n" ^

   310   "(4, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy , pen2str, Position.T))]"

   311 (*MISSING: ------------------------------------------------------------------- (b_b, y)          *)

   312 then () else error "init_pstate initial i_model CHANGED";

   313 \<close> ML \<open> (*isa*)

   314     val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;

   315 (*?! complete with Met.i_model ?!*)

   316 \<close> ML \<open> (*isa*)

   317 (*+*)if (env_model |> Subst.to_string @{context}) = "[\"\n" ^

   318   "(q__q, q_0)\", \"\n" ^

   319   "(v_v, x)\", \"\n" ^

   320   "(id_der, dy)\", \"\n" ^

   321   "(fun_s, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)])\"]"

   322 then () else error "init_pstate: env_model CHANGED";

   323 \<close> ML \<open> (*isa*)

   324     val actuals = map snd env_model

   325 \<close> text \<open> (*isa2*)

   326     val (_, env_subst, env_eval) = I_Model.of_max_variant model_patt i_model;

   327     val actuals = map snd env_subst

   328 \<close> ML \<open> (*isa==isa2*)

   329 (*+*)val "[q_0, x, dy, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]"

   330  = actuals |> UnparseC.terms @{context}

   331 \<close> ML \<open> (*isa==isa2*)

   332     val formals = Program.formal_args prog

   333 \<close> ML \<open> (*isa==isa2*)

   334 (*+*)val "[q__q, v_v, b_b, id_der]" = formals |> UnparseC.terms @{context} (*From fun. belastung_zu_biegelinie*)

   335 \<close> ML \<open> (*isa*)

   336     val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))

   337     val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

   338 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   339     val ist = Istate.e_pstate

   340       |> Istate.set_eval prog_rls

   341       |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)

   342 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   343           (relate_args [] formals actuals ctxt prog met_id formals actuals);

   344 \<close> ML \<open>

   345 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   346   ([], formals, actuals, ctxt, prog, met_id, formals, actuals);

   348     (*if*) type_of f = type_of a (*then*);

   349 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   350            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

   351 \<close> ML \<open>

   352 (*+*)val "q__q" = f |> UnparseC.term @{context}

   353 (*+*)val "q_0" = a |> UnparseC.term @{context};

   354 \<close> ML \<open>

   355     (*if*) type_of f = type_of a (*then*);

   356 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   357            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

   358 \<close> ML \<open>

   359 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   360   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

   361 \<close> ML \<open>

   362 (*+*)val "v_v" = f |> UnparseC.term @{context}

   363 (*+*)val "x" = a |> UnparseC.term @{context}

   364 \<close> ML \<open>

   365     (*if*) type_of f = type_of a (*then*);

   366 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   367            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

   368 \<close> ML \<open>

   369 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   370   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

   371 \<close> ML \<open>

   372 (*+*)val "b_b" = f |> UnparseC.term @{context} (*ERROR: IS Biegelinie*)

   373 (*+*)val "dy" = a |> UnparseC.term @{context}  (*ERROR: IS AbleitungBiegelinie*)

   374 (*CONCLUSION: if the type is equal, then the sequence decides the pairing for env

   375   (q__q, q_0)

   376   (v_v, x)

   377 *)

   378 \<close> ML \<open>

   379     (*if*) type_of f = type_of a (*then*);

   380 \<close> ML \<open>

   381 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   382            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

   383 \<close> ML \<open>

   384 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   385   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

   386 \<close> ML \<open>

   387 (*+*)val "id_der" = f |> UnparseC.term @{context} (*ERROR IS AbleitungBiegelinie*)

   388 (*+*)val "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

   389  = a |> UnparseC.term @{context}                  (*ERROR IS FROM Pbl.i_model*)

   390 \<close> ML \<open>

   391     (*if*) type_of f = type_of a (*else*);

   392 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   393         val (f, a) =

   394            assoc_by_type ctxt f aas prog met_id formals actuals;

   395 \<close> ML \<open>

   396 "~~~~~ fun assoc_by_type , args:"; val (ctxt, f, aa, prog, met_id, formals, actuals) =

   397   (ctxt, f, aas, prog, met_id, formals, actuals);

   398 \<close> ML \<open>

   399 val [] =

   400   (*case*) filter (curry (fn (f, a) => type_of f = type_of a) f) aa (*of*);

   401 \<close> ML \<open>

   402 (*+*)val Free ("id_der", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])) = f

   403 \<close> ML \<open>

   404 (*+*)val [Const ("List.list.Cons", _) $ _ $

   405       (Const ("List.list.Cons", _) $ _ $

   406         (Const ("List.list.Cons", _) $ _ $

   407           (Const ("List.list.Cons", _) $ _ $

   408             Const ("List.list.Nil", list_elem_type))))] = aa

   409 (*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = list_elem_type

   410 \<close> ML \<open>

   411 \<close> ML \<open>

   412 \<close> ML \<open>

   413 \<close> ML \<open>

   414 \<close> ML \<open>

   415 \<close> ML \<open>

   416 \<close> ML \<open>

   417 \<close> ML \<open>

   418 \<close> ML \<open>

   419 \<close> ML \<open> (*||----------- continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)

   420 (*||------------------ continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)

   421 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

   422 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

   423 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   424 val (p,_,f,nxt,_,pt) = return_me_Add_Given_AbleitungBiegelinie;

   425 \<close> ML \<open>

   426 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

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

   428 *)

   429 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",

   430    UNDETECTED BY Test_Isac_Short.thy

   431 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   432 arguments_from_model: 'Biegelinie' not in itms:

   433 itms:

   434 [

   435 (1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),

   436 (2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),

   437 (3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [

   438   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   439   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   440   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   441   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],

   442  (funs''', [[

   443   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   444   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   445   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   446   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),

   447 (4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]

   448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   449 CORRECTION:

   450 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   451 Const ("Biegelinie.Biegelinie", _) MUST BE IN itms OF THE model,

   452 BECAUSE REQUIRED BY GUARD OF MethodC.

   453 *)

   454 (*//---------------- adhoc inserted ------------------------------------------------\\*)

   455 \<close> ML \<open>

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

   457       val (pt, p) =

   458   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   459   	    case Step.by_tactic tac (pt, p) of

   460   		    ("ok", (_, _, ptp)) => ptp

   461   	    | ("unsafe-ok", (_, _, ptp)) => ptp

   462   	    | ("not-applicable",_) => (pt, p)

   463   	    | ("end-of-calculation", (_, _, ptp)) => ptp

   464   	    | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"

   465   	    | _ => raise ERROR "me: uncovered case Step.by_tactic";

   466 \<close> ML \<open>

   468 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   469   	     (*case*)

   470       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

   471 *)

   472 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =

   473   (p, ((pt, Pos.e_pos'), []));

   474   (*if*) Pos.on_calc_end ip (*else*);

   475       val (_, probl_id, _) = Calc.references (pt, p);

   476 val _ =

   477       (*case*) tacis (*of*);

   478         (*if*) probl_id = Problem.id_empty (*else*);

   480 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   481            switch_specify_solve p_ (pt, ip)

   482 *)

   483 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

   484       (*if*) Pos.on_specification ([], state_pos) (*then*);

   486 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   487            specify_do_next (pt, input_pos)

   488 *)

   489 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

   490     val (_, (p_', tac)) = Specify.find_next_step ptp

   491     val ist_ctxt =  Ctree.get_loc pt (p, p_)

   492 val Tactic.Apply_Method mI =

   493     (*case*) tac (*of*);

   495 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   496   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'))

   497 *)

   498 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =

   499 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

   500          val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of

   501            PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

   502          | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

   503          val {model, ...} = MethodC.from_store ctxt mI;

   504          val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

   505          val prog_rls = LItool.get_simplifier (pt, pos);

   507 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   508           (*case*)

   509     LItool.init_pstate prog_rls ctxt itms mI (*of*);

   510 *)

   511 "~~~~~ fun init_pstate , args:"; val (prog_rls, ctxt, itms, metID) = (prog_rls, ctxt, itms, mI);

   512 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)

   513     val actuals =

   514            arguments_from_model metID itms

   515 *)

   516 \<close> ML \<open>

   517 "~~~~~ fun arguments_from_model , args:"; val (mI, itms) = (metID, itms);

   518     val mvat = Pre_Conds.max_variant itms

   519     fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b

   520     val itms = filter (okv mvat) itms;

   522 I_Model.to_string @{context} itms |> writeln;

   523 (*[

   524 (1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),

   525 (2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),

   526 (3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [

   527   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   528   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   529   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   530   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],

   531  (funs''', [[

   532   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   533   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   534   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   535   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),

   536 (4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]

   537 *)

   538     fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.descriptor itm_)

   539     fun itm2arg itms (_, (d, _)) =

   540       case find_first (test_dsc d) itms of

   541         NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)

   542       | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_

   544     val pats = (#model o MethodC.from_store ctxt) mI;

   545 (*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))),

   546     ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),

   547     ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("b_b", "real \<Rightarrow> real"))),

   548     ("#Given", (Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_der", "real \<Rightarrow> real"))),

   549     ("#Find", (Const ("Biegelinie.Funktionen", "bool list \<Rightarrow> una"), Free ("fun_s", "bool list")))]:

   550    Model_Pattern.T*)

   551 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)

   552        (flat o (map (

   553            itm2arg itms))) pats

   554 *)

   555 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 1 pats);

   556 val SOME (1, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) =

   557         find_first (test_dsc d) itms;

   559 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 2 pats);

   560 val SOME (2, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v_v", _), [Free ("x", _)]))) =

   561         find_first (test_dsc d) itms;

   563 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 3 pats);

   564 val Const ("Biegelinie.Biegelinie", _) = d

   565 val NONE =

   566         find_first (test_dsc d) itms;

   568 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 4 pats);

   569 val SOME (4, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", _), [Free ("dy", _)]), (Free ("id_der", _), [Free ("dy", _)]))) =

   570         find_first (test_dsc d) itms;

   572 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 5 pats);

   573 val SOME (3, [1], true, "#Find", Cor ((Const ("Biegelinie.Funktionen", _), _), (Free ("funs'''", _), _))) =

   574         find_first (test_dsc d) itms

   576 (*\\---------------- adhoc inserted ------------------------------------------------//*)

   577 \<close> ML \<open>

   578 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",

   579    UNDETECTED BY Test_Isac_Short.thy ===========================================================\\

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   608 		   "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

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

   610 		   "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

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

   612 		   "- EI * y'' x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

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

   614 		   "y'' x = 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)";

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

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

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

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

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

   620     "y' x = Integral 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";

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

   622 "y' x = Integral 1 / (- 1 * EI) * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";

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

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

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

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

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

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

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

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

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

   632 "y x =\nIntegral c_3 +\n         1 / (- 1 * EI) *\n         (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x";

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

   634 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";

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

   636    "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";

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

   638 if f2str f =

   639    "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

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

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

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

   643 =============================================================================================//*)

   645 \<close> ML \<open>

   646 \<close>

   648 section \<open>===================================================================================\<close>

   649 section \<open>=====  ============================================================================\<close>

   650 ML \<open>

   651 \<close> ML \<open>

   653 \<close> ML \<open>

   654 \<close>

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

   657 ML \<open>

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

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

   660 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

   661 "~~~~~ continue fun xxx"; val () = ();

   662 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

   663 "xx"

   664 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

   665 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

   666  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

   667 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

   668 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

   670 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

   671 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

   672 (*keep for continuing YYYYY*)

   673 \<close> ML \<open> (*------------- continue XXXXX --------------------------------------------------------*)

   674 (*-------------------- continue XXXXX --------------------------------------------------------*)

   675 (*kept for continuing XXXXX*)

   676 (*-------------------- stop step into XXXXX --------------------------------------------------*)

   677 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

   678 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

   679 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

   681 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

   682 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

   683 (*/------------------- check within XXXXX ---------------------------------------------------\*)

   684 (*\------------------- check within XXXXX ---------------------------------------------------/*)

   685 (*/------------------- check result of XXXXX ------------------------------------------------\*)

   686 (*\------------------- check result of XXXXX ------------------------------------------------/*)

   687 (* final test ... ----------------------------------------------------------------------------*)

   689 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

   690 (*//------------------ inserted hidden code ------------------------------------------------\\*)

   691 (*\\------------------ inserted hidden code ------------------------------------------------//*)

   692 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

   694 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

   695 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

   696 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

   697 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

   698 \<close>

   699 end

author	wneuper <Walther.Neuper@jku.at>
	Sun, 20 Aug 2023 08:54:01 +0200
changeset 60735	2d17dac14264
parent 60730	a36ce69b2315
child 60736	7297c166991e
permissions	-rw-r--r--