wneuper/isa: test/Tools/isac/Test_Theory.thy@5e91c279af3a

     1 (* use this theory for tests before Build_Isac.thy has succeeded *)

     2 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

     3   "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

     4 begin

     5 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

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

     8 text \<open>

     9   declare [[show_types]]

    10   declare [[show_sorts]]

    11   find_theorems "?a <= ?a"

    13   print_theorems

    14   print_facts

    15   print_statement ""

    16   print_theory

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

    18   declare [[ML_print_depth = 999]]

    19   declare [[ML_exception_trace]]

    20 \<close>

    21 (** )

    22   (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

    23 ( **)

    24 ML \<open>

    25 \<close> ML \<open>

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

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

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

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

    30 (*if*) (*then*); (*else*); (*andalso*)  (*case*) (*of*);  (*return value*);

    31 (*let*) (*in*) (*end*); (*map:*)

    32 "xx"^ "xxx"   (*+*) (*+++*) (*isa*) (*isa2*) (**)

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

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

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

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

    39 \<close> ML \<open> (*--------------locate below ~~~ fun XXXXX, asap shift into separate section above ----*)

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

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

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

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

    45 \<close> ML \<open> (*//----------- setup test data for XXXXX -------------------------------------------\\*)

    46 (*//------------------ setup test data for XXXXX -------------------------------------------\\*)

    47 (*\\------------------ setup test data for XXXXX -------------------------------------------//*)

    48 \<close> ML \<open> (*\\----------- setup test data for XXXXX -------------------------------------------//*)

    50 (* final test ... ----------------------------------------------------------------------------*)

    52 \<close> ML \<open> (*=== not needed @{context} \<longrightarrow> ctxt except args of init_calc*)

    53 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

    54 (*-------------------- there must not be > ML < inbetween-------------------------------------*)

    55 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

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

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

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

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

    63 (** )val calling_code =( **)

    64 (**)val return_XXXXX =(**)

    65   "call XXXXX";

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

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

    68 \<close> ML \<open> (*||----------- contine.. XXXXX -------------------------------------------------------*)

    69 (*||------------------ contine.. XXXXX -------------------------------------------------------*)

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

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

    72 val calling_code = return_XXXXX;

    74 (*=== complete model for step into (the above is optimised wrt. quick replacement fo XXXXX)*)

    75 (** )val calling_code =( **)

    76 (**)val return_XXXXX =(**)

    77   "call XXXXX";

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

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

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

    81 \<close> ML \<open> (*||----------- contine.. XXXXX -------------------------------------------------------*)

    82 (*||------------------ contine.. XXXXX -------------------------------------------------------*)

    83 val return_XXXXX_STEP = 123

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

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

    86 val calling_code = return_XXXXX;

    88 (*=== rules for step into:

    89  * XXXXX = me_specify_step_by_tactic  ...i.e. include stucture id in identifiers

    90  * val return_XXXXX_STEP = return_YYYYY

    91    ... indicates, that the value of a called function is also the value of the calling function

    92  *)

    93 \<close> ML \<open>

    94 \<close>

    96 section \<open>===================================================================================\<close>

    97 section \<open>=====  ============================================================================\<close>

    98 ML \<open>

    99 \<close> ML \<open>

   101 \<close> ML \<open>

   102 \<close>

   104 (** )ML_file "Knowledge/eqsystem-1.sml"( **)

   105 section \<open>===================================================================================\<close>

   106 section \<open>===== Knowledge/eqsystem-1.sml ====================================================\<close>

   107 section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>

   108 ML \<open>

   109 (* Title: Knowledge/eqsystem-1.sml

   110    author: Walther Neuper 050826,

   111    (c) due to copyright terms

   112 *)

   114 "-----------------------------------------------------------------------------------------------";

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

   116 "-----------------------------------------------------------------------------------------------";

   117 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

   118 "----------- problems -----------------------------------------------------------equsystem-1.sml";

   119 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

   120 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

   121 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

   122 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

   123 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

   124 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

   125 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

   126 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

   127 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";

   128 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   129 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

   130 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

   131 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";

   132 "-----------------------------------------------------------------------------------------------";

   133 "-----------------------------------------------------------------------------------------------";

   134 "-----------------------------------------------------------------------------------------------";

   136 val thy = @{theory "EqSystem"};

   137 val ctxt = Proof_Context.init_global thy;

   139 open Kernel

   140 open Tactic

   141 open Test_Code

   142 open Pos

   143 open P_Model

   144 open Rewrite;

   145 open Prog_Expr;

   147 "----------- occur_exactly_in ------------------------------------";

   148 "----------- occur_exactly_in ------------------------------------";

   149 "----------- occur_exactly_in ------------------------------------";

   150 val all = [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"];

   151 val t = ParseC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

   153 if occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2"] all t

   154 then () else error "eqsystem.sml occur_exactly_in 1";

   156 if not (occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"] all t)

   157 then () else error "eqsystem.sml occur_exactly_in 2";

   159 if not (occur_exactly_in [ParseC.parse_test @{context}"c_2"] all t)

   160 then () else error "eqsystem.sml occur_exactly_in 3";

   162 val t = ParseC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

   163 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   164 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   165 if str = "[c, c_2] from [c, c_2,\n" ^

   166   "               c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"

   167 then () else error "eval_occur_exactly_in [c, c_2]";

   169 val t = ParseC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^

   170 		  "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");

   171 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   172 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^

   173 "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"

   174 then () else error "eval_occur_exactly_in [c, c_2, c_3]";

   176 val t = ParseC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \

   177 		\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

   178 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   179 if str = "[c_2] from [c, c_2,\n" ^

   180   "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"

   181 then () else error "eval_occur_exactly_in [c, c_2, c_3]";

   183 val t = ParseC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";

   184 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   185 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()

   186 else error "eval_occur_exactly_in [c, c_2, c_3]";

   188 val t =

   189     ParseC.parse_test @{context}

   190 	"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";

   191 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

   192 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \

   193 	 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()

   194 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";

   197 "----------- problems --------------------------------------------";

   198 "----------- problems --------------------------------------------";

   199 "----------- problems --------------------------------------------";

   200 val t = ParseC.parse_test @{context} "Length [x+y=1,y=2] = 2";

   201 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty

   202 			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),

   203 			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),

   204 			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),

   205 			  Eval (\<^const_name>\<open>HOL.eq\<close>, eval_equal "#equal_")

   206 			  ];

   207 val SOME (t',_) = rewrite_set_ ctxt false testrls t;

   208 if UnparseC.term @{context} t' = "True" then ()

   209 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";

   211 val SOME t = ParseC.term_opt ctxt "solution LL";

   212 TermC.atom_trace_detail @{context} t;

   213 val SOME t = ParseC.term_opt ctxt "solution LL";

   214 TermC.atom_trace_detail @{context} t;

   216 val t = ParseC.parse_test @{context}

   217 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";

   218 TermC.atom_trace_detail @{context} t;

   219 val t = ParseC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^

   220   "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");

   221 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\

   222         assume flawed test setup hidden by "handle _ => ..."

   223         ERROR rewrite__set_ called with 'Erls' for '1 < 1'

   224 val SOME (t,_) =

   225     rewrite_set_ ctxt true

   226 		 (Rule_Set.append_rules "prls_" Rule_Set.empty

   227 			     [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),

   228 			      Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),

   229 			      Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),

   230 			      Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),

   231 			      Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")

   232 			      ]) t;

   233 if t = @{term True} then ()

   234 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";

   235         broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)

   238 "----------- rewrite-order ord_simplify_System -------------------";

   239 "----------- rewrite-order ord_simplify_System -------------------";

   240 "----------- rewrite-order ord_simplify_System -------------------";

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

   242 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)

   243 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",

   244 				       ParseC.parse_test @{context}"c * x") then ()

   245 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";

   247 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",

   248 				       ParseC.parse_test @{context}"c_2") then ()

   249 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";

   251 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"c * x",

   252 				       ParseC.parse_test @{context}"c_2") then ()

   253 else error "integrate.sml, (c * x) < (c_2) not#3";

   255 "--- mult.commute ---";

   256 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"x * c",

   257 				       ParseC.parse_test @{context}"c * x") then ()

   258 else error "integrate.sml, (x * c) < (c * x) not#4";

   260 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",

   261 				       ParseC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")

   262 then () else error "integrate.sml, (. * .) < (. * .) not#5";

   264 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",

   265 				       ParseC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")

   266 then () else error "integrate.sml, (. * .) < (. * .) not#6";

   269 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";

   270 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";

   271 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";

   272 val t = ParseC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\

   273 	        \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";

   274 val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),

   275 	    (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];

   276 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

   277 if UnparseC.term @{context} t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"

   278 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";

   280 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

   281 if UnparseC.term @{context} t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"

   282 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";

   284 val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;

   285 if UnparseC.term @{context} t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"

   286 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";

   288 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";

   289 val SOME (t,_) = rewrite_set_ ctxt true order_system t;

   290 if UnparseC.term @{context} t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"

   291 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";

   294 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

   295 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

   296 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

   297 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);

   298 val ctxt = Proof_Context.init_global thy;

   299 val t =

   300     ParseC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +         \

   301 	    \                                     - 1 * q_0 / 24 * 0 \<up> 4),\

   302 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +         \

   303 	    \                                     - 1 * q_0 / 24 * L \<up> 4)]";

   304 val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;

   305 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

   306                       "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)

   307                       "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"

   308 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";

   310 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

   311 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

   312                        "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)

   313                        "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"

   314 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";

   316 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

   317 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

   318                        "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)

   319                        "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"

   320 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";

   322 val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;

   323 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

   324                        "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)

   325                        "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"

   326 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";

   328 val xxx = rewrite_set_ ctxt true order_system t;

   329 if is_none xxx

   330 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";

   333 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

   334 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

   335 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

   336 val e1__ = ParseC.parse_test @{context} "c_2 = 77";

   337 val e2__ = ParseC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";

   338 val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),

   339 	    (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];

   340 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;

   341 if UnparseC.term @{context} e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()

   342 else error "eqsystem.sml top_down_substitution,2x2] subst";

   344 val SOME (e2__,_) =

   345     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;

   346 if UnparseC.term @{context} e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()

   347 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";

   349 val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;

   350 if UnparseC.term @{context} e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()

   351 else error "eqsystem.sml top_down_substitution,2x2] isolate";

   353 val t = ParseC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";

   354 val SOME (t,_) = rewrite_set_ ctxt true order_system t;

   355 if UnparseC.term @{context} t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()

   356 else error "eqsystem.sml top_down_substitution,2x2] order_system";

   358 if not (ord_simplify_System

   359 	    false ctxt []

   360 	    (ParseC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",

   361 	     ParseC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))

   362 then () else error "eqsystem.sml, order_result rew_ord";

   365 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";

   366 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";

   367 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";

   368 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)

   369 val t = ParseC.parse_test @{context} (

   370   "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^

   371   "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^

   372   "c + c_2 + c_3 + c_4 = 0, " ^

   373   "c_2 + c_3 + c_4 = 0]");

   374 val bdvs = [(ParseC.parse_test @{context}"bdv_1::real",ParseC.parse_test @{context}"c::real"),

   375 	    (ParseC.parse_test @{context}"bdv_2::real",ParseC.parse_test @{context}"c_2::real"),

   376 	    (ParseC.parse_test @{context}"bdv_3::real",ParseC.parse_test @{context}"c_3::real"),

   377 	    (ParseC.parse_test @{context}"bdv_4::real",ParseC.parse_test @{context}"c_4::real")];

   378 val SOME (t, _) =

   379     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

   380 if UnparseC.term @{context} t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"

   381 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";

   383 val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

   384 if UnparseC.term @{context} t = "[c_4 = 0, \

   385 	        \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \

   386 		\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"

   387 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";

   389 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

   390 if UnparseC.term @{context} t = "[c_4 = 0,\

   391 		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\

   392 		\ c + (c_2 + (c_3 + c_4)) = 0,\n\

   393 		\ c_2 + (c_3 + c_4) = 0]"

   394 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";

   396 val SOME (t, _) = rewrite_set_ ctxt true order_system t;

   397 if UnparseC.term @{context} t = "[c_4 = 0,\

   398 		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\

   399 		\ c_2 + (c_3 + c_4) = 0,\n\

   400 		\ c + (c_2 + (c_3 + c_4)) = 0]"

   401 then () else error "eqsystem.sml rewrite in 4x4 order_system";

   404 "----------- refine [linear,system]-------------------------------";

   405 "----------- refine [linear,system]-------------------------------";

   406 "----------- refine [linear,system]-------------------------------";

   407 val fmz =

   408   ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^

   409                "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",

   410 	   "solveForVars [c, c_2]", "solution LL"];

   412 (*WN120313 in "solution L" above "Refine.by_formalise @{context} fmz ["LINEAR", "system"]" caused an error...*)

   413 "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);

   414 "~~~~~ fun check_match' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =

   415    ((rev o tl) pblID, fmz, [(*match list*)],

   416      ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));

   417       val {thy, model, where_, where_rls, ...} = py ;

   418 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);

   419       val (ts, ctxt) = ContextC.init_while_parsing fmz thy;

   420 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);

   421       fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of

   422               (_, _::_) => (Free (v,T)::get_vars vs)

   423             | (_, []  ) => get_vars vs) (*filter out nums as long as

   424                                           we have Free ("123",_)*)

   425         | get_vars [] = [];

   426                                         t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^

   427                                             "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";

   428       val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

   429 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;

   430 val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;

   431 val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;

   432 val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;

   433                                         val t = nth 2 fmz; t = "solveForVars [c, c_2]";

   434       val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

   435 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;

   436                                         val t = nth 3 fmz; t = "solution LL";

   437       (*(Syntax.read_term ctxt t);

   438 Type unification failed: Clash of types "real" and "_ list"

   439 Type error in application: incompatible operand type

   441 Operator:  solution :: bool list \<Rightarrow> toreall

   442 Operand:   L :: real                 ========== L was already present in equalities ========== *)

   444 "===== case 1 =====";

   445 val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];

   446 case matches of

   447  [M_Match.Matches (["LINEAR", "system"], _),                      (*Matches*)

   448   M_Match.Matches (["2x2", "LINEAR", "system"], _),               (*NoMatch !--> continue search !*)

   449   M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)

   450   M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],      (**)

   451     {Find = [Correct "solution LL"], With = [],                   (**)

   452     Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

   453              Correct "solveForVars [c, c_2]"],

   454     Where = [],

   455     Relate = []})] => ()

   456 | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";

   458 "===== case 2 =====";

   459 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

   460 	   "solveForVars [c, c_2]", "solution LL"];

   461 val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];

   462 case matches of [_,_,

   463 		  M_Match.Matches

   464 		    (["triangular", "2x2", "LINEAR", "system"],

   465 		      {Find = [Correct "solution LL"],

   466 		       With = [],

   467 		       Given =

   468 		        [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

   469 		         Correct "solveForVars [c, c_2]"],

   470 		       Where = [Correct

   471 			"tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n      [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

   472 			                Correct

   473 				"[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n   [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],

   474 		       Relate = []})] => ()

   475 | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";

   477 (*WN051014-----------------------------------------------------------------------------------\\

   478   the above 'val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"]'

   479   didn't work anymore; we investigated in these steps:*)

   480 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

   481 	  "solveForVars [c, c_2]", "solution LL"];

   482 val matches = Refine.by_formalise @{context} fmz ["triangular", "2x2", "LINEAR", "system"];

   483 (*... resulted in

   484    False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n

   485           [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)

   486 val t = ParseC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^

   487 		  "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");

   489 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;

   490 (*found:...

   491 ##  try thm: NTH_CONS

   492 ###  eval asms: 1 < 2 + - 1

   493 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =

   494     nth_ (2 + - 1 + - 1) []

   495 ####  rls: erls_prls_triangular on: 1 < 2 + - 1

   496 #####  try calc: op <'

   497 ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + - 1"]

   499 ... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)

   500 (*--------------------------------------------------------------------------------------------//*)

   503 "===== case 3: relaxed preconditions for triangular system =====";

   504 val fmz = ["equalities [L * q_0 = c,                               \

   505 	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\

   506 	   \            0 = c_4,                                           \

   507 	   \            0 = c_3]",

   508 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

   509 (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:

   510 probably exn thrown by fun declare_constraints

   511 /-------------------------------------------------------\

   512 Type unification failed

   513 Type error in application: incompatible operand type

   515 Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list

   516 Operand:   [c_4] :: 'b list

   517 \-------------------------------------------------------/

   518 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];

   519 case TermC.matches of

   520     [M_Match.Matches (["LINEAR", "system"], _),

   521      M_Match.NoMatch (["2x2", "LINEAR", "system"], _),

   522      M_Match.NoMatch (["3x3", "LINEAR", "system"], _),

   523      M_Match.Matches (["4x4", "LINEAR", "system"], _),

   524      M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),

   525      M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()

   526   | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";

   527 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)

   529 "===== case 4 =====";

   530 val fmz = ["equalities [L * q_0 = c,                                       \

   531 	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\

   532 	   \            0 = c_3,                           \

   533 	   \            0 = c_4]",

   534 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

   535 val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];

   536 case TermC.matches of

   537     [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()

   538   | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";

   539 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];

   540 ============ inhibit exn WN120314 ==============================================*)

   543 "----------- Refine.refine [2x2,linear,system] search error--------------";

   544 "----------- Refine.refine [2x2,linear,system] search error--------------";

   545 "----------- Refine.refine [2x2,linear,system] search error--------------";

   546 (*didn't go into ["2x2", "LINEAR", "system"];

   547   we investigated in these steps:*)

   548 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\

   549 	               \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

   550 	   "solveForVars [c, c_2]", "solution LL"];

   551 val matches = Refine.by_formalise @{context} fmz ["2x2", "LINEAR", "system"];

   552 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)

   553 (*brought: 'False "length_ es_ = 2"'*)

   555 (*-----fun check_match' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =

   556 (* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =

   557        (rev ["LINEAR", "system"], fmz, [(*match list*)],

   558 	((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));

   559    *)

   560 > show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;

   561 val it = "length_ (es_::real list) = (2::real)" : string

   563 =========================================================================\

   564 -------fun Problem.prep_input

   565 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,

   566 		  ev:rls, ca: string option, metIDs:metID list)) =

   567        (EqSystem.thy, (["system"],

   568 		       [("#Given" ,["equalities es_", "solveForVars v_s"]),

   569 			("#Find"  ,["solution ss___"](*___ is copy-named*))

   570 			],

   571 		       Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],

   572 		       SOME "solveSystem es_ v_s",

   573 		       []));

   574    *)

   575 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;

   576 val equalities_es_ = "equalities es_" : string

   577 > val (dd, ii) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o (TermC.parse thy)) equalities_es_;

   578 > show_types:=true; UnparseC.term @{context} ii; show_types:=false;

   579 val it = "es_::bool list" : string

   580 ~~~~~~~~~~~~~~~ \<up> \<up> \<up>  OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   582 > val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];

   583 > show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;

   585 =========================================================================/

   587 -----fun check_match' ff:

   588 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;

   589 [

   590 (1 ,[1] ,true ,#Given ,Cor equalities

   591  [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

   592   0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

   593  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),

   594 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),

   595 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]

   597 > (writeln o pres2str) pre';

   598 [

   599 (false, length_ es_ = 2),

   600 (true, length_ [c, c_2] = 2)]

   602 ----- fun match_oris':

   603 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;

   604 > (writeln o pres2str) pre';

   605 ..as in check_match'

   607 ----- fun check in Pre_Conds.

   608 > (writeln o env2str) env;

   609 ["

   610 (es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

   611  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "

   612 (v_s, [c, c_2])", "

   613 (ss___, L)"]

   615 > val es_ = (fst o hd) env;

   616 val es_ = Free ("es_", "bool List.list") : Term.term

   618 > val pre1 = hd pres;

   619 TermC.atom_trace_detail @{context} pre1;

   620 ***

   621 *** Const (op =, [real, real] => bool)

   622 *** . Const (ListG.length_, real list => real)

   623 *** . . Free (es_, real list)

   624 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up>  should be bool list~~~~~~~~~~~~~~~~~~~

   625 *** . Free (2, real)

   626 ***

   628 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM

   629 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   630 *)

   633 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

   634 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

   635 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

   636 (*this test fails, see TODO WN230404*)

   637 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^

   638                        "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

   639 	   "solveForVars [c, c_2]", "solution LL"];

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

   641   ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],

   642    ["EqSystem", "normalise", "2x2"]);

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

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

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

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

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

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

   649 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt

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

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

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

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

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

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

   656 case nxt of

   657     (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()

   658   | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";

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

   661 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0]" = nxt

   662 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt

   663 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt

   664 \<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)

   665 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

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

   668 val xxx = nxt

   670 val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt;

   672 (*ERROR WN230404: mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])"*)

   673 (** )val return_Add_Given_equ

   674                      = me nxt p c pt;( **)

   675 (*//------------------ step into Add_Given_equ ---------------------------------------------\\*);

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

   677       val ctxt = Ctree.get_ctxt pt p

   678 val ("ok", (_, _, (pt, p))) =

   679   	    (*case*) Step.by_tactic tac (pt, p) (*of*);

   681 (** )          (*case*)

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

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

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

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

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

   687 val _ =

   688       (*case*) tacis (*of*);

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

   691 (** )      switch_specify_solve p_ (pt, ip);( **)

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

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

   695 (** )      specify_do_next (pt, input_pos);( **)

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

   698 (** )val (_, (p_', tac)) =

   699    Specify.find_next_step ptp;( **)

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

   702 (** )val (_, (p_', tac)) =

   703    Specify.find_next_step ptp;( **);

   704 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

   705     val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

   706       spec = refs, ...} = Calc.specify_data (pt, pos);

   707     val ctxt = Ctree.get_ctxt pt pos;

   708       (*if*)  Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

   709         (*if*) p_ = Pos.Pbl (*then*);

   711 (** )Specify.for_problem ctxt oris (o_refs, refs) (pbl, met); ( **)

   712 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

   713   (ctxt, oris, (o_refs, refs), (pbl, met));

   714     val cpI = if pI = Problem.id_empty then pI' else pI;

   715     val cmI = if mI = MethodC.id_empty then mI' else mI;

   716     val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

   717     val {model = mpc, ...} = MethodC.from_store ctxt cmI

   719 (** )val (preok, _) =

   720  Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); ( **);

   721 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

   722   (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));

   724 (*WN230827: REPLACE WITH I_Model.of_max_variant* )val (env_subst, env_eval) =

   725            sep_variants_envs_OLD model_patt i_model ( **)

   726 "~~~~~ fun sep_variants_envs_OLD , args:"; val (model_patt, i_model) = (model_patt, i_model);

   727     val equal_descr_pairs =

   728       map (get_equal_descr i_model) model_patt

   729       |> flat

   730     val all_variants =

   731         map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs

   732         |> flat

   733         |> distinct op =

   734     val variants_separated = map (filter_variants equal_descr_pairs) all_variants

   735     val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>

   736       m_field = "#Given")) variants_separated;

   738 (** )val envs_subst = map

   739            mk_env_subst restricted_to_given ( **)

   740 "~~~~~ fun mk_env_subst , args:"; val (equal_descr_pairs) = (nth 1 (nth 1 restricted_to_given));

   742 val xxx =

   743 (*+*)(fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

   744         => (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id))

   745       : Model_Pattern.single * I_Model.single_TEST -> Pre_Conds.env_subst;

   746 (*+*)equal_descr_pairs: Model_Pattern.single * I_Model.single_TEST;

   748 (** )      xxx equal_descr_pairs ( **)

   749 "~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (equal_descr_pairs);

   750 (*ERROR WN230404 (see TODO.md:

   751 mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])" (**)

   752           (mk_env feedb) *)

   754 (*+*)feedb: Model_Def.i_model_feedback_TEST;

   755 (*+*)(*----^^^^^^^^^^^^^^^^^^*)

   756 (*+*)  I_Model.Cor_TEST: (descriptor * term list) * (term * term list) -> feedback_TEST;

   757 (*+*)Model_Def.Cor_TEST: (descriptor * term list) * (term * term list) -> Model_Def.i_model_feedback_TEST;

   758 (*\\------------------ step into Add_Given_equ ---------------------------------------------//*)

   761 val (p,_,f,nxt,_,pt) = return_Add_Given_equ; (**)val Add_Given "solveForVars [c]" = nxt;(**)

   762 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2]" = nxt;

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

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

   766 case nxt of

   767     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

   768   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";

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

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

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

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

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

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

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

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

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

   779 case nxt of

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

   781   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";

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

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

   784 (* final test ... ----------------------------------------------------------------------------*)

   785 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()

   786 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";

   788 case nxt of

   789     (End_Proof') => ()

   790   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

   792 Test_Tool.show_pt pt (*[

   793 (([], Frm), solveSystem

   794  [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],

   795   [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]

   796  [[c], [c_2]]),

   797 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

   798  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),

   799 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),

   800 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),

   801 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),

   802 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),

   803 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),

   804 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),

   805 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),

   806 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),

   807 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),

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

   809 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),

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

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

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

   813 *)

   814 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

   816 \<close> ML \<open>

   817 \<close>

   819 section \<open>===================================================================================\<close>

   820 section \<open>===== Knowledge/eqsystem-1a.sml ===================================================\<close>

   821 section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>

   822 ML \<open>

   823 (* Title: Knowledge/eqsystem-1a.sml

   824    author: Walther Neuper 050826,

   825 *)

   827 "-----------------------------------------------------------------------------------------------";

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

   829 "-----------------------------------------------------------------------------------------------";

   830 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

   831 "----------- problems -----------------------------------------------------------equsystem-1.sml";

   832 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

   833 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

   834 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

   835 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

   836 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

   837 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

   838 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

   839 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

   840 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";

   841 (*========== ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^--vvvvvvvvvvvvvvvv ==================*)

   842 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   843 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

   844 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

   845 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";

   846 "-----------------------------------------------------------------------------------------------";

   847 "-----------------------------------------------------------------------------------------------";

   848 "-----------------------------------------------------------------------------------------------";

   851 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   852 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   853 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   854 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^

   855                        "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

   856 	   "solveForVars [c, c_2]", "solution LL"];

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

   858   ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],

   859    ["EqSystem", "normalise", "2x2"]);

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

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

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

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

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

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

   866 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()

   867 	  | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";

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

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

   872 (*+*)if f2str f =

   873   "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^

   874   " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";

   875 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt) =

   876    "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";

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

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

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

   881 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt

   882                                       val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;

   883 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)"

   884  = (Ctree.get_istate_LI pt p |> Istate.string_of ctxt)

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

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

   888 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt

   889 \<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)

   890 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

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

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

   893 case nxt of

   894     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

   895   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";

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

   899   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   900 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);

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

   903 (*/------------------- step into me Apply_Method -------------------------------------------\*)

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

   905       val (pt'''', p'''') = (* keep for continuation*)

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

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

   909   		    ("ok", (_, _, ptp)) => ptp;

   910 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

   912 (*+isa==isa2*)val ([5], Met) = p;

   913 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);

   914   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   915 (*+isa==isa2*)is1 |> Istate.string_of ctxt;

   916   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   917 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);

   919   (*case*)

   920       Step.check tac (pt, p) (*of*);

   921 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );

   923 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   924 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);

   926   (*if*) Tactic.for_specify tac (*else*);

   927 val Applicable.Yes xxx =

   929 Solve_Step.check tac (ctree, pos);

   931 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   932 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);

   934 "~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);

   935 	    (*if*)  Tactic.for_specify' tac' (*else*);

   937 Step_Solve.by_tactic tac' ptp;;

   938 "~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))

   939   = (tac', ptp);

   941 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   942 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);

   944         LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;

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

   946   = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);

   947          val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

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

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

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

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

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

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

   955 (*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =

   956 (*+isa==isa2*)is |> Istate.string_of ctxt

   958         val ini = LItool.implicit_take ctxt prog env;

   959         val pos = start_new_level pos

   960 val NONE =

   961         (*case*) ini (*of*);

   962             val (tac''', ist''', ctxt''') =

   963    case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of

   964                 Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)

   966   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   967 (*+isa==isa2*)ist''' |> Istate.string_of ctxt;

   969 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

   970   = (prog ,(pt, (lev_dn p, Res)), is, ctxt);

   971 val Accept_Tac

   972     (Take' ttt, iii, _) =

   973   (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

   975 (*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term @{context});

   976   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   977 (*+isa==isa2*)(Pstate iii |> Istate.string_of ctxt);

   979 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

   980   = ((prog, (ptp, ctxt)), (Pstate ist));

   981   (*if*) path = [] (*then*);

   983            scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

   984 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

   985   = (cc, (trans_scan_dn ist), (Program.body_of prog));

   987   (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

   988 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

   989   = (cc ,(ist |> path_down [L, R]), e);

   991   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =

   992 (*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);

   994     (*if*) Tactical.contained_in t (*else*);

   996       (*case*)

   997     LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

   998 "~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)

   999   = ("next  ", ctxt, eval, (get_subst ist), t);

  1001     (*case*)

  1002   Prog_Tac.eval_leaf E a v t (*of*);

  1003 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))

  1004   = (E, a, v, t);

  1006 val return =

  1007      (Program.Tac (subst_atomic E t), NONE:term option);

  1008 "~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;

  1009 	        val stac' = Rewrite.eval_prog_expr ctxt prog_rls

  1010               (subst_atomic (Env.update_opt E (a, v)) stac)

  1012 val return =

  1013       (Program.Tac stac', a');

  1014 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;

  1016            check_tac cc ist (prog_tac, form_arg);

  1017 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

  1018   = (cc, ist, (prog_tac, form_arg));

  1019     val m = LItool.tac_from_prog (pt, p) prog_tac

  1020 val _ =

  1021     (*case*) m (*of*); (*tac as string/input*)

  1023       (*case*)

  1024 Solve_Step.check m (pt, p) (*of*);

  1025 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));

  1027 val return =

  1028     check_tac cc ist (prog_tac, form_arg)

  1030   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =

  1031 (*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);

  1033 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";

  1034        val (Accept_Tac (tac, ist, ctxt)) = return;

  1036   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

  1037 (*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt)

  1039 val return =

  1040       Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);

  1041 "~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;

  1042             val (tac', ist', ctxt') = (tac, ist, ctxt)

  1043 val Tactic.Take' t =

  1044             (*case*) tac' (*of*);

  1045                   val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');

  1047 (*+isa==isa2*)pos; (*from check_tac*)

  1048 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];

  1049   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

  1050 (*+isa==isa2*)is1 |> Istate.string_of ctxt;

  1051   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

  1052 (*+isa==isa2*)(ist' |> Istate.string_of ctxt)

  1053 (*-------------------- stop step into me Apply_Method ----------------------------------------*)

  1054 (*+isa==isa2*)val "c_2 = 0" = f2str f;

  1055   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

  1056 (*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of ctxt)

  1057 (*\\------------------- step into me Apply_Method ------------------------------------------//*)

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

  1061 (*+isa==isa2*)val ([5, 1], Frm) = p'''';

  1062 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;

  1063 (*+isa<>isa2*)val (** )Check_Postcond ["triangular", "2x2", "LINEAR", "system"]( **)

  1064                        Substitute ["c_2 = 0"](**) = nxt'''';

  1065 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');

  1066   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

  1067 (*+isa==isa2*)is1 |> Istate.string_of ctxt;

  1068   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

  1069 (*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of ctxt;

  1071 (*//------------------ step into me Take ---------------------------------------------------\\*)

  1072 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');

  1074       val (pt, p) = (* keep for continuation*)

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

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

  1078   		    ("ok", (_, _, ptp)) => ptp;

  1080   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

  1081 (*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of ctxt;

  1083     (*case*)

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

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

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

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

  1088 val _ =

  1089       (*case*) tacis (*of*);

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

  1092            switch_specify_solve p_ (pt, ip);

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

  1094       (*if*) Pos.on_specification ([], state_pos) (*else*);

  1096         LI.do_next (pt, input_pos);

  1097 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);

  1098     (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

  1099         val thy' = get_obj g_domID pt (par_pblobj pt p);

  1100 	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

  1102   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

  1103 (*+isa==isa2*)ist |> Istate.string_of ctxt;

  1105         (*case*)

  1106         LI.find_next_step sc (pt, pos) ist ctxt (*of*);

  1107 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

  1108   = (sc, (pt, pos), ist, ctxt);

  1110   (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

  1111 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

  1112   = ((prog, (ptp, ctxt)), (Pstate ist));

  1113   (*if*) path = [] (*else*);

  1115            go_scan_up (prog, cc) (trans_scan_up ist);

  1116 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  1117   = ((prog, cc), (trans_scan_up ist));

  1119   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =

  1120 (*+isa==isa2*)Pstate ist |> Istate.string_of ctxt;

  1121 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term @{context};

  1123     (*if*) path = [R] (*root of the program body*) (*else*);

  1125            scan_up pcc (ist |> path_up) (go_up ctxt path sc);

  1126 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))

  1127   = (pcc, (ist |> path_up), (go_up ctxt path sc));

  1128         val (i, body) = check_Let_up ctxt ist sc;

  1130   (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);

  1131 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

  1132   = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);

  1134 val goback =

  1135   (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

  1136 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))

  1137   = (cc, (ist |> path_down [L, R]), e);

  1139   (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

  1140 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

  1141   = (cc, (ist |> path_down_form ([L, L, R], a)), e1);

  1142         (*if*) Tactical.contained_in t (*else*);

  1144       (*case*)

  1145     LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

  1146 "~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)

  1147   = ("next  ", ctxt, eval, (get_subst ist), t);

  1148 val (Program.Tac stac, a') =

  1149     (*case*) Prog_Tac.eval_leaf E a v t (*of*);

  1150 	        val stac' = Rewrite.eval_prog_expr ctxt prog_rls

  1151               (subst_atomic (Env.update_opt E (a, v)) stac)

  1153 (*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term @{context};

  1155 val return =

  1156         (Program.Tac stac', a');

  1157 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))

  1158    = (return);

  1160            check_tac cc ist (prog_tac, form_arg);

  1161 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

  1162   = (cc, ist, (prog_tac, form_arg));

  1163     val m = LItool.tac_from_prog (pt, p) prog_tac

  1164 val _ =

  1165     (*case*) m (*of*);

  1167      (*case*)

  1168 Solve_Step.check m (pt, p) (*of*);

  1169 "~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))

  1170   = (m, (pt, p));

  1171         val pp = Ctree.par_pblobj pt p

  1172         val ctxt = Ctree.get_loc pt pos |> snd

  1173         val thy = Proof_Context.theory_of ctxt

  1174         val f = Calc.current_formula cs;

  1175 		    val {rew_ord, asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)

  1176 		    val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube

  1177 		    val ro = get_rew_ord ctxt rew_ord;

  1178 		    (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);

  1180 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term @{context}

  1181 (*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map (UnparseC.term @{context})

  1183 val SOME ttt =

  1184 		      (*case*) Rewrite.rewrite_terms_ ctxt ro asm_rls subte f (*of*);

  1185 (*-------------------- stop step into me Take ------------------------------------------------*)

  1186 (*\\------------------ step into me Take ---------------------------------------------------//*)

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

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

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

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

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

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

  1195 (*+*)val (** )"L * c + c_2 = q_0 * L \<up> 2 / 2"( **)

  1196              "[c = L * q_0 / 2, c_2 = 0]"(**) = f2str f;

  1197 (*val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =*)

  1198   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =

  1199 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);

  1201 case nxt of

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

  1203   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";

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

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

  1207 (* final test ... ----------------------------------------------------------------------------*)

  1208 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()

  1209 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";

  1211 case nxt of

  1212     (End_Proof') => ()

  1213   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

  1215 Test_Tool.show_pt pt (*[

  1216 (([], Frm), solveSystem

  1217  [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],

  1218   [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]

  1219  [[c], [c_2]]),

  1220 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

  1221  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),

  1222 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),

  1223 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),

  1224 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),

  1225 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),

  1226 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),

  1227 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),

  1229 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),

  1230 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),

  1231 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),

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

  1233 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),

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

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

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

  1237 *)

  1238 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

  1240 \<close> ML \<open>

  1241 \<close>

  1243 section \<open>===================================================================================\<close>

  1244 section \<open>===== Knowledge/eqsystem-2.sml ====================================================\<close>

  1245 section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>

  1246 ML \<open>

  1247 (* Title: Knowledge/eqsystem-2.sml

  1248    author: Walther Neuper 050826,

  1249    (c) due to copyright terms

  1250 *)

  1251 "-----------------------------------------------------------------------------------------------";

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

  1253 "-----------------------------------------------------------------------------------------------";

  1254 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

  1255 "----------- problems -----------------------------------------------------------equsystem-1.sml";

  1256 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

  1257 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

  1258 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

  1259 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

  1260 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

  1261 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

  1262 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

  1263 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

  1264 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";

  1265 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

  1266 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

  1267 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

  1268 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";

  1269 "-----------------------------------------------------------------------------------------------";

  1270 "-----------------------------------------------------------------------------------------------";

  1271 "-----------------------------------------------------------------------------------------------";

  1273 val thy = @{theory "EqSystem"};

  1274 val ctxt = Proof_Context.init_global thy;

  1276 "----------- me [linear,system] ..normalise..top_down_sub..-------";

  1277 "----------- me [linear,system] ..normalise..top_down_sub..-------";

  1278 "----------- me [linear,system] ..normalise..top_down_sub..-------";

  1279 val fmz =

  1280     ["equalities\

  1281      \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +                \

  1282      \                                            - 1 * q_0 / 24 * 0 \<up> 4),\

  1283      \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +                \

  1284      \                                            - 1 * q_0 / 24 * L \<up> 4)]",

  1285      "solveForVars [c, c_2]", "solution LL"];

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

  1287   ("Biegelinie",["LINEAR", "system"], ["no_met"]);

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

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

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

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

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

  1293 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["normalise", "2x2", "LINEAR", "system"] = nxt

  1294                                       val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt

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

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

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

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

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

  1300 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt

  1301                                       val "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]" = f2str f;

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

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

  1304 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt

  1305 \<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)

  1306 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

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

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

  1310 case nxt of

  1311     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

  1312   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";

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

  1315 val PblObj {probl,...} = get_obj I pt [5];

  1316     (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;

  1317 (*[

  1318 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),

  1319 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),

  1320 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]

  1321 *)

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

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

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

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

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

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

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

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

  1330 case nxt of

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

  1332   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";

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

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

  1336 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..

  1337   "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)

  1338   "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"

  1339 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";

  1340 case nxt of

  1341     (End_Proof') => ()

  1342   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

  1343 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

  1346 \<close> ML \<open>

  1347 "----------- all systems from Biegelinie -------------------------";

  1348 "----------- all systems from Biegelinie -------------------------";

  1349 "----------- all systems from Biegelinie -------------------------";

  1350 val thy = @{theory Isac_Knowledge}

  1351 val subst =

  1352   [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"), (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),

  1353 	(ParseC.parse_test @{context} "bdv_3", ParseC.parse_test @{context} "c_3"), (ParseC.parse_test @{context} "bdv_4", ParseC.parse_test @{context} "c_4")];

  1355 "------- Bsp 7.27";

  1356 States.reset ();

  1357 CalcTree @{context} [(

  1358   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1359 	  "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],

  1360 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];

  1361 \<close> ML \<open>(*ERROR type_of: type mismatch in application,  real, real list, occurs_in [c]*)

  1362 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

  1363 moveActiveRoot 1;

  1364 (*

  1365 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1366 ##7.27##          ordered           substs

  1367           c_4       c_2

  1368 c c_2 c_3 c_4     c c_2             1->2: c

  1369   c_2                       c_4

  1370 c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)

  1371 val t = ParseC.parse_test @{context}

  1372   ("[0 = c_4, " ^

  1373   "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^

  1374   "0 = c_2, " ^

  1375   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");

  1376 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;

  1377 if UnparseC.term @{context} t =

  1378 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"

  1379 then () else error "Bsp 7.27";

  1381 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";

  1382 val t = ParseC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";

  1383 val NONE = rewrite_set_ ctxt false norm_Rational t;

  1384 val SOME (t,_) =

  1385     rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

  1386 if UnparseC.term @{context} t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"

  1387 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";

  1389 "--- isolate_bdvs_4x4";

  1390 (*

  1391 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;

  1392 UnparseC.term @{context} t;

  1393 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;

  1394 UnparseC.term @{context} t;

  1395 val SOME (t,_) = rewrite_set_ ctxt false order_system t;

  1396 UnparseC.term @{context} t;

  1397 *)

  1399 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1400 States.reset ();

  1401 CalcTree @{context} [((*WN130908  <ERROR> error in kernel </ERROR>*)

  1402   ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",

  1403 	    "Biegelinie y",

  1404 	    "Randbedingungen [y L = 0, y' L = 0]",

  1405 	    "FunktionsVariable x"],

  1406 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

  1407 	    ["Biegelinien", "AusMomentenlinie"]))];

  1408 (*

  1409 moveActiveRoot 1;

  1410 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1411 *)

  1413 "------- Bsp 7.69";

  1414 States.reset ();

  1415 CalcTree @{context} [(

  1416   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1417 	  "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],

  1418 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];

  1419 moveActiveRoot 1;

  1420 (*

  1421 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1422 ##7.69##          ordered           subst                   2x2

  1423           c_4           c_3

  1424 c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2

  1425       c_3                   c_4

  1426 c c_2 c_3         c c_2 c_3 c_4     3:c_4 -> 4:c c_2 c_3    1:c_3 -> 4:c c_2*)

  1427 val t = ParseC.parse_test @{context}

  1428   ("[0 = c_4 + 0 / (- 1 * EI), " ^

  1429   "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^

  1430   "0 = c_3 + 0 / (- 1 * EI), " ^

  1431   "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");

  1433 "------- Bsp 7.70";

  1434 States.reset ();

  1435 CalcTree @{context} [(

  1436   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1437 	  "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],

  1438 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];

  1439 moveActiveRoot 1;

  1440 (*

  1441 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1442 ##7.70##        |subst

  1443 c		|

  1444 c c_2           |1:c -> 2:c_2

  1445       c_3	|

  1446           c_4   |            STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)

  1448 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";

  1449 val t = ParseC.parse_test @{context}

  1450   ("[L * q_0 = c, " ^

  1451   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^

  1452   "0 = c_4, " ^

  1453   "0 = c_3]");

  1454 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

  1455 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

  1456 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

  1457 if UnparseC.term @{context} t =

  1458   "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"

  1459 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";

  1461 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

  1462 if UnparseC.term @{context} t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"

  1463 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";

  1465 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;

  1466 if UnparseC.term @{context} t =

  1467    "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^

  1468    " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"

  1469 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";

  1471 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

  1472 if UnparseC.term @{context} t =

  1473   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"

  1474 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";

  1476 val SOME (t, _) = rewrite_set_ ctxt false order_system t;

  1477 if UnparseC.term @{context} t =

  1478   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"

  1479 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";

  1481 "----- 7.70 with met normalise: ";

  1482 val fmz = ["equalities" ^

  1483   "[L * q_0 = c, " ^

  1484   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^

  1485   "0 = c_4, " ^

  1486   "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

  1487 val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);

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

  1490 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==

  1491   in next but one test below the same type error.

  1492 /-------------------------------------------------------\

  1493 Type unification failed

  1494 Type error in application: incompatible operand type

  1496 Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list

  1497 Operand:   [c_4] :: 'b list

  1498 \-------------------------------------------------------/

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

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

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

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

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

  1505 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()

  1506 	  | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";

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

  1509 "----- outcommented before Isabelle2002 --> 2011 -------------------------";

  1510 (*-----------------------------------vvvWN080102 Exception- Match raised

  1511   since associate Rewrite .. Rewrite_Set

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

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

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

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

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

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

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

  1521 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"

  1522 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";

  1523 --------------------------------------------------------------------------*)

  1524 ============ inhibit exn WN120314 ==============================================*)

  1526 "----- 7.70 with met top_down_: me";

  1527 val fmz = [

  1528   "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",

  1529 	"solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];

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

  1531   ("Biegelinie",["LINEAR", "system"],["no_met"]);

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

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

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

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

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

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

  1538 case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()

  1539 	  | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";

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

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

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

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

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

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

  1546 if p = ([], Res) andalso

  1547 (*           "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)

  1548    f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

  1549 then () else error "eqsystem.sml: 7.70 with met top_down_: me";

  1551 "------- Bsp 7.71";

  1552 States.reset ();

  1553 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1554 	     "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",

  1555 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  1556 	     "AbleitungBiegelinie dy"],

  1557 	    ("Biegelinie", ["Biegelinien"],

  1558 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1559 moveActiveRoot 1;

  1560 (*

  1561 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1562 ##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal

  1563 c c_2          |c c_2	      |1'		      |1': c c_2 |

  1564           c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |

  1565 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

  1566       c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)

  1567 val t = ParseC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \

  1568 \ 0 = c_4 + 0 / (- 1 * EI),                            \

  1569 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\

  1570 \ 0 = c_3 + 0 / (- 1 * EI)]";

  1572 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1573 States.reset ();

  1574 CalcTree @{context} [(["Traegerlaenge L",

  1575 	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",

  1576 	    "Biegelinie y",

  1577 	    "Randbedingungen [y 0 = (0::real), y L = 0]",

  1578 	    "FunktionsVariable x"],

  1579 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

  1580 	    ["Biegelinien", "AusMomentenlinie"]))];

  1581 moveActiveRoot 1;

  1582 (*

  1583 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1584 *)

  1586 "------- Bsp 7.72b";

  1587 States.reset ();

  1588 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",

  1589 	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",

  1590 	    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  1591 	    "AbleitungBiegelinie dy"],

  1592 	   ("Biegelinie", ["Biegelinien"],

  1593 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

  1594 moveActiveRoot 1;

  1595 (*

  1596 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1597 ##7.72b##      |ord. |subst.singles         |ord.triang.

  1598   c_2          |     |			    |c_2

  1599 c c_2	       |     |1:c_2 -> 2':c	    |c_2 c

  1600           c_4  |     |			    |

  1601 c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)

  1602 val t = ParseC.parse_test @{context}"[0 = c_2,                                            \

  1603 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \

  1604 \ 0 = c_4 + 0 / (- 1 * EI),                            \

  1605 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";

  1607 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1608 States.reset ();

  1609 CalcTree @{context} [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)

  1610 	    "Biegelinie y",

  1611 	    "Randbedingungen [y L = 0, y' L = 0]",

  1612 	    "FunktionsVariable x"],

  1613 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

  1614 	    ["Biegelinien", "AusMomentenlinie"]))];

  1615 moveActiveRoot 1;

  1616 (*

  1617 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

  1618 *)

  1620 "----------- 4x4 systems from Biegelinie -------------------------";

  1621 "----------- 4x4 systems from Biegelinie -------------------------";

  1622 "----------- 4x4 systems from Biegelinie -------------------------";

  1623 (*STOPPED.WN08?? replace this test with 7.70 *)

  1624 "----- Bsp 7.27";

  1625 val fmz = ["equalities \

  1626 	   \[0 = c_4,                           \

  1627 	   \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI),                                       \

  1628 	   \ 0 = c_2,                                           \

  1629 	   \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",

  1630 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

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

  1632   ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],

  1633    ["EqSystem", "normalise", "4x4"]);

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

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

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

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

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

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

  1640 "------------------------------------------- Apply_Method...";

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

  1642 "[0 = c_4,                                          \

  1643 \ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI),                                   \

  1644 \ 0 = c_2,                                          \

  1645 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";

  1646 (*vvvWN080102 Exception- Match raised

  1647   since associate Rewrite .. Rewrite_Set

  1648 "------------------------------------------- simplify_System_parenthesized...";

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

  1650 "[0 = c_4,                                  \

  1651 \ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) +     \

  1652 \     (4 * L \<up> 3 * c / (- 24 * EI) +       \

  1653 \     (12 * L \<up> 2 * c_2 / (- 24 * EI) +    \

  1654 \     (L * c_3 + c_4))),                    \

  1655 \ 0 = c_2,                                  \

  1656 \ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";

  1657 (*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)

  1658 "------------------------------------------- isolate_bdvs...";

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

  1660 "[c_4 = 0,\

  1661 \ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\

  1662 \ c_2 = 0, \

  1663 \ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";

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

  1666 ---------------------------------------------------------------------*)

  1667 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

  1669 \<close> ML \<open>

  1670 \<close>

  1672 (** )ML_file "Specify/specify.sml"( **)

  1673 section \<open>===================================================================================\<close>

  1674 section \<open>===== Specify/specify.sml =========================================================\<close>

  1675 section \<open>===== (*ERROR isalist2list applied to NON-list: funs'''*) =========================\<close>

  1676 ML \<open>

  1677 (* Title:  "Specify/specify.sml"

  1678    Author: Walther Neuper

  1679    (c) due to copyright terms

  1680 *)

  1682 "-----------------------------------------------------------------------------------------------";

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

  1684 "-----------------------------------------------------------------------------------------------";

  1685 "-----------------------------------------------------------------------------------------------";

  1686 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";

  1687 "----------- revise Specify.do_all -------------------------------------------------------------";

  1688 "----------- specify-phase: low level functions for Biegelinie ---------------------------------";

  1689 "-----------------------------------------------------------------------------------------------";

  1690 "-----------------------------------------------------------------------------------------------";

  1691 "-----------------------------------------------------------------------------------------------";

  1692 open Pos;

  1693 open Ctree;

  1694 open Test_Code;

  1695 open Tactic;

  1696 open Specify;

  1697 open Step;

  1699 open O_Model;

  1700 open I_Model;

  1701 open P_Model;

  1702 open Specify_Step;

  1703 open Test_Code;

  1705 (**** maximum-example: Specify.finish_phase  ############################################# ****)

  1706 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";

  1707 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";

  1708 (*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )

  1709  val (p,_,f,nxt,_,pt) =

  1710      Test_Code.init_calc @{context}

  1711      [(["fixedValues [r=Arbfix]", "maximum A",

  1712 	"valuesFor [a,b]",

  1713 	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

  1714 	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

  1715 	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

  1717 	"boundVariable a", "boundVariable b", "boundVariable alpha",

  1718 	"interval {x::real. 0 <= x & x <= 2*r}",

  1719 	"interval {x::real. 0 <= x & x <= 2*r}",

  1720 	"interval {x::real. 0 <= x & x <= pi}",

  1721 	"errorBound (eps=(0::real))"],

  1722        ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])

  1723        )];

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

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

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

  1727  (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)

  1728  val pits = get_obj g_pbl pt (fst p);

  1729  writeln (I_Model.to_string ctxt pits);

  1730 (*[

  1731 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

  1732 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),

  1733 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

  1734 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)

  1735  val (pt,p) = Specify.finish_phase (pt,p);

  1736  val pits = get_obj g_pbl pt (fst p);

  1737  if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"

  1738  then () else error "completetest.sml: new behav. in Specify.finish_phase 3";

  1739  writeln (I_Model.to_string ctxt pits);

  1740 (*[

  1741 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

  1742 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

  1743 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

  1744 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up>

  1745 2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)

  1746  val mits = get_obj g_met pt (fst p);

  1747  if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"

  1748  then () else error "completetest.sml: new behav. in Specify.finish_phase 3";

  1749  writeln (I_Model.to_string ctxt mits);

  1750 (*[

  1751 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

  1752 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

  1753 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

  1754 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up>

  1755 2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),

  1756 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

  1757 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

  1758 0 <= x & x <= 2 * r}])),

  1759 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

  1760 ( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)

  1763 (**** revise Specify.do_all ############################################################## ****);

  1764 "----------- revise Specify.do_all -------------------------------------------------------------";

  1765 "----------- revise Specify.do_all -------------------------------------------------------------";

  1766 (* from Minisubplb/100-init-rootpbl.sml:

  1767 val (_(*example text*),

  1768   (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::

  1769      "Extremum (A = 2 * u * v - u \<up> 2)" ::

  1770      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::

  1771      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::

  1772      "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::

  1773      "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::

  1774      "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

  1775      "ErrorBound (\<epsilon> = (0::real))" :: []),

  1776    refs as ("Diff_App",

  1777      ["univariate_calculus", "Optimisation"],

  1778      ["Optimisation", "by_univariate_calculus"])))

  1779   = Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

  1780 *)

  1781 val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::

  1782      "Extremum (A = 2 * u * v - u \<up> 2)" ::

  1783      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::

  1784      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::

  1785      "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::

  1786      "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::

  1787      "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

  1788      "ErrorBound (\<epsilon> = (0::real))" :: [])

  1789 val refs = ("Diff_App",

  1790      ["univariate_calculus", "Optimisation"],

  1791      ["Optimisation", "by_univariate_calculus"])

  1793 val (p,_,f,nxt,_,pt) =

  1794  Test_Code.init_calc @{context} [(model, refs)];

  1795 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])

  1796   = (@{context}, [(model, refs)]);

  1798    Specify.do_all (pt, p);

  1799 (*//------------------ step into do_all ----------------------------------------------------\\*)

  1800 "~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);

  1801     val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of

  1802       Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}

  1803         => (itms, oris, probl, o_spec, spec, ctxt)

  1804     | _ => raise ERROR "LI.by_tactic: no PblObj"

  1805     val (_, pbl_id', met_id') = References.select_input o_refs spec

  1806     val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris

  1807       (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id', met_id')

  1808 ;

  1809 (*-------------------- stop step into do_all -------------------------------------------------*)

  1810 (*/------------------- check result of I_Model.complete' ------------------------------------\*)

  1811 (*+*)if Model_Pattern.to_string @{context} (#model (MethodC.from_store ctxt met_id')) = "[\"" ^

  1812   "(#Given, (Constants, fixes))\", \"" ^

  1813   "(#Given, (Maximum, maxx))\", \"" ^

  1814   "(#Given, (Extremum, extr))\", \"" ^

  1815   "(#Given, (SideConditions, sideconds))\", \"" ^

  1816   "(#Given, (FunctionVariable, funvar))\", \"" ^

  1817   "(#Given, (Input_Descript.Domain, doma))\", \"" ^

  1818   "(#Given, (ErrorBound, err))\", \"" ^

  1819   "(#Find, (AdditionalValues, vals))\"]"

  1820 (*+*)then () else error "mod_pat CHANGED";

  1821 (*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^

  1822   "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^

  1823   "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^

  1824   "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^

  1825   "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^

  1826   "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^

  1827   "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^

  1828   "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^

  1829   "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

  1830 (*+*)then () else error "met_imod CHANGED";

  1831 (*\------------------- check result of I_Model.complete' ------------------------------------/*)

  1832 (*\\------------------ step into do_all ----------------------------------------------------//*)

  1834 (*-------------------- continuing do_all -----------------------------------------------------*)

  1835     val (pt, _) = Ctree.cupdate_problem pt p

  1836       (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)

  1837 ;

  1840 (**** specify-phase: low level functions for Biegelinie #################################### ****)

  1841 "----------- specify-phase: low level functions for Biegelinie ---------------------------------";

  1842 "----------- specify-phase: low level functions for Biegelinie ---------------------------------";

  1843 open Pos;

  1844 open Ctree;

  1845 open Test_Code;

  1846 open Tactic;

  1847 open Specify;

  1848 open Step;

  1850 open O_Model;

  1851 open I_Model;

  1852 open P_Model;

  1853 open Specify_Step;

  1855 val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

  1856 	    "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

  1857 (*

  1858   Now follow items for ALL SubProblems,

  1859   since ROOT MethodC must provide values for "actuals" of ALL SubProblems.

  1860   See Biegelinie.thy subsection \<open>Survey on Methods\<close>.

  1861 *)

  1862 (*

  1863   Items for MethodC "IntegrierenUndKonstanteBestimmen2"

  1864 *)

  1865 	    "FunktionsVariable x",

  1866     (*"Biegelinie y",          ..already input for Problem above*)

  1867       "AbleitungBiegelinie dy",

  1868       "Biegemoment M_b",

  1869       "Querkraft Q",

  1870 (*

  1871   Item for Problem "LINEAR/system", which by [''no_met''] involves refinement

  1872 *)

  1873       "GleichungsVariablen [c, c_2, c_3, c_4]"

  1874 ];

  1875 (*

  1876   Note: the above sequence of items follows the sequence of formal arguments (and of model items)

  1877   of MethodC "IntegrierenUndKonstanteBestimmen2"

  1878 *)

  1879 val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

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

  1881 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)

  1883 (*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)

  1884 (*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =

  1885   get_obj g_origin pt (fst p);

  1886 (*+*)if O_Model.to_string @{context} o_model = "[\n" ^

  1887   "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

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

  1889   "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  1890   "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  1891   "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  1892   "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^

  1893   "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^

  1894   "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^

  1895   "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"

  1896 then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";

  1897 (*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)

  1899 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt

  1900 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt

  1901 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt

  1902 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0]" = nxt

  1903 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0]" = nxt

  1904 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0]" = nxt

  1905 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y L = 0, y 0 = 0, M_b 0 = 0, M_b L = 0]" = nxt

  1907 val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)

  1908 (*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)

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

  1910       val ctxt = Ctree.get_ctxt pt p

  1911       val (pt, p) =

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

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

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

  1916 val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =

  1917       (*case*)

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

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

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

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

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

  1923 val _ =

  1924       (*case*) tacis (*of*);

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

  1927            switch_specify_solve p_ (pt, ip);

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

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

  1931            specify_do_next (pt, input_pos);

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

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

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

  1935 val Specify_Theory "Biegelinie" =

  1936           (*case*) tac (*of*);

  1938 Step_Specify.by_tactic_input tac (pt, (p, p_'));

  1940 (*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)

  1941 (*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)

  1942 (*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;

  1943                                                  val Specify_Theory "Biegelinie" = nxt

  1944 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt

  1945 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

  1947 (*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2

  1948                                 = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)

  1949 \<close> ML \<open>(*/------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)

  1950 (*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)

  1952 (*/------------------- initial check for whole me ------------------------------------------\*)

  1953 (*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;

  1955 (*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =

  1956   Calc.specify_data (pt, p);

  1957 (*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])

  1958 (*+*)then () else error "initial o_refs CHANGED";

  1959 (*+*)if O_Model.to_string @{context} o_model = "[\n" ^

  1960   "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

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

  1962   "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  1963   "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  1964   "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  1965   "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^

  1966   "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^

  1967   "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^

  1968   "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"

  1969 (*+*)then () else error "initial o_model CHANGED";

  1970 (*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str)]"

  1971  = I_Model.to_string @{context} i_pbl

  1972 (*+*)val "[]" = I_Model.to_string @{context} i_met

  1973 (*+*)val (_, ["Biegelinien"], _) = spec;

  1974 (*\------------------- initial check for whole me ------------------------------------------/*)

  1976 \<close> ML \<open>(*//------------ step into Step.by_tactic -------------------------------------------\\*)

  1977 (*//------------------ step into Step.by_tactic -------------------------------------------\\*)

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

  1979       val (pt'''''_', p'''''_') = case

  1980       Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;

  1981 (*/------------------- check for entry to Step.by_tactic -----------------------------------\*)

  1982 (*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;

  1983 (*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);

  1984 (*+*)if O_Model.to_string @{context} o_model = "[\n" ^

  1985   "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

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

  1987   "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  1988   "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  1989   "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  1990   "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^

  1991   "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^

  1992   "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^

  1993   "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"

  1994 (*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";

  1995 (*\------------------- check for Step.by_tactic --------------------------------------------/*)

  1996 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  1997   val Applicable.Yes (tac' as Specify_Method' (["IntegrierenUndKonstanteBestimmen2"], o_model, i_model)) =(*case*)

  1998       Step.check tac (pt, p) (*of*);

  1999 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));

  2000   (*if*) Tactic.for_specify tac (*then*);

  2002 Specify_Step.check tac (ctree, pos);

  2003 "~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));

  2005         val (o_model''''', _, i_model''''') =

  2006            Specify_Step.complete_for mID (ctree, pos);

  2007 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));

  2008     val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,

  2009        ...} = Calc.specify_data (ctree, pos);

  2010     val ctxt = Ctree.get_ctxt ctree pos

  2011     val (dI, _, _) = References.select_input o_refs refs;

  2012     val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

  2013     val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))

  2015     val (o_model', ctxt') =

  2016    O_Model.complete_for m_patt root_model (o_model, ctxt);

  2017 (*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)

  2018 (*+*)Model_Pattern.to_string @{context}  m_patt = "[\"" ^

  2019   "(#Given, (Traegerlaenge, l))\", \"" ^

  2020   "(#Given, (Streckenlast, q))\", \"" ^

  2021   "(#Given, (FunktionsVariable, v))\", \"" ^

  2022   "(#Given, (GleichungsVariablen, vs))\", \"" ^

  2023   "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^

  2024   "(#Find, (Biegelinie, b))\", \"" ^

  2025   "(#Relate, (Randbedingungen, s))\"]";

  2026 (*+*) O_Model.to_string @{context} root_model;

  2027 (*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)

  2028 "~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));

  2029     val  missing = m_patt |> filter_out

  2030       (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))

  2031 \<close> ML \<open>

  2032 (*ERROR?*)val [] = missing

  2033 \<close> ML \<open>

  2034     val add = (root_model

  2035       |> filter

  2036         (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))

  2037 ;

  2038 val return_complete_for =

  2039     ((o_model @ add)

  2040       |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

  2041       |> map (fn (_, b, c, d, e) => (b, c, d, e))      (* for correct enumeration *)

  2042       |> add_enumerate                                        (* for correct enumeration *)

  2043       |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)

  2044     ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);

  2045 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =

  2046     ((o_model @ add)

  2047       |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

  2048       |> map (fn (_, b, c, d, e) => (b, c, d, e))      (* for correct enumeration *)

  2049       |> add_enumerate                                        (* for correct enumeration *)

  2050       |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)

  2051     ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));

  2052 (*+*)val "[\n(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n(4, [\"1\"], #Given, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n(6, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"]), \n(7, [\"1\"], #Given, Biegemoment, [\"M_b\"]), \n(8, [\"1\"], #Given, Querkraft, [\"Q\"]), \n(9, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"

  2053  =  O_Model.to_string @{context} o_model';

  2055     val thy = ThyC.get_theory @{context} dI

  2056     val (_, (i_model, _)) = M_Match.match_itms_oris ctxt o_model'

  2057       (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST met_imod) (m_patt, where_, where_rls) ;

  2059 val return_Specify_Step_complete_for =

  2060   (o_model', ctxt', i_model);

  2062 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =

  2063   (o_model', ctxt', i_model);

  2065 val return_Specify_Step_check =

  2066    Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD  i_model));

  2067 "~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =

  2068   (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model)));

  2069 	    (*if*) Tactic.for_specify' tac' (*then*);

  2070   val ("ok", ([], [], (_, _))) =

  2072 Step_Specify.by_tactic tac' ptp;

  2073 "~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =

  2074   (tac', ptp);

  2075   val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,

  2076      ...} = Calc.specify_data (pt, pos);

  2077   val (dI, _, mID) = References.select_input o_refs refs;

  2078   val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

  2079   val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))

  2080   val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)

  2081   val thy = ThyC.get_theory @{context} dI

  2082   val (_, (i_model, _)) = M_Match.match_itms_oris ctxt o_model'

  2083     (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_meth) (m_patt, where_, where_rls);

  2084   val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', I_Model.TEST_to_OLD i_model))

  2085     (Istate_Def.Uistate, ctxt') (pt, pos)

  2087 (*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)

  2088 (*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);

  2089 (*+*)O_Model.to_string @{context} o_model;

  2090 (*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str), \n(0 ,[1] ,false ,i_model_empty ,Sup FunktionsVariable), \n(0 ,[1] ,false ,i_model_empty ,Sup AbleitungBiegelinie), \n(0 ,[1] ,false ,i_model_empty ,Sup Biegemoment), \n(0 ,[1] ,false ,i_model_empty ,Sup Querkraft), \n(0 ,[1] ,false ,i_model_empty ,Sup GleichungsVariablen []), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str)]"

  2091  = I_Model.to_string @{context} meth

  2092 (*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)

  2093 (*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)

  2095 val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

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

  2097 (*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)

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

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

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

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

  2102      val _ = (*case*) tacis (*of*);

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

  2105 val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

  2106          switch_specify_solve p_ (pt, ip);

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

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

  2110 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =

  2111       Step.specify_do_next (pt, input_pos);

  2112 (*/------------------- check result of specify_do_next -------------------------------------\*)

  2113 (*+*)val {origin = (ooo_mod, _, _), meth, ...} =  Calc.specify_data (pt'''''_'', p'''''_'');

  2114 (*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";

  2115 (*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str), \n(0 ,[1] ,false ,i_model_empty ,Sup AbleitungBiegelinie), \n(0 ,[1] ,false ,i_model_empty ,Sup Biegemoment), \n(0 ,[1] ,false ,i_model_empty ,Sup Querkraft), \n(0 ,[1] ,false ,i_model_empty ,Sup GleichungsVariablen []), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str)]"

  2116  = I_Model.to_string @{context} meth;

  2117 (*\------------------- check result of specify_do_next -------------------------------------/*)

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

  2120 (**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)

  2121    Specify.find_next_step ptp;

  2122 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

  2123     val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

  2124       spec = refs, ...} = Calc.specify_data (pt, pos);

  2125     val ctxt = Ctree.get_ctxt pt pos;

  2126     (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);

  2127       (*if*) p_ = Pos.Pbl (*else*);

  2129 val return_XXX = for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met);

  2130 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  2131   (oris, (o_refs, refs), (pbl, met));

  2132     val cmI = if mI = MethodC.id_empty then mI' else mI;

  2133     val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;

  2134     val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);

  2135 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return_XXX);

  2136 (*/------------------- check within find_next_step -----------------------------------------\*)

  2137 (*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^

  2138   "(#Given, (Traegerlaenge, l))\", \"" ^

  2139   "(#Given, (Streckenlast, q))\", \"" ^

  2140   "(#Given, (FunktionsVariable, v))\", \"" ^   (* <---------- take m_field from here !!!*)

  2141   "(#Given, (GleichungsVariablen, vs))\", \"" ^

  2142   "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^

  2143   "(#Find, (Biegelinie, b))\", \"" ^

  2144   "(#Relate, (Randbedingungen, s))\"]";

  2145 (*\------------------- check within find_next_step -----------------------------------------/*)

  2147 val return_item_to_add as SOME ("#Given", "FunktionsVariable x") =

  2148     (*case*) item_to_add ctxt oris (I_Model.OLD_to_TEST met) (*of*);

  2149 "~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =

  2150   (ctxt, oris, mpc, I_Model.OLD_to_TEST met);

  2151 val SOME (fd, ct') = return_item_to_add

  2153 (*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';

  2155 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =

  2156   ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));

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

  2158     val _ = (*case*) tac (*of*);

  2160       ("dummy",

  2161 Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);

  2162 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =

  2163   (tac, (pt, (p, p_')));

  2165   val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

  2166      Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);

  2167 "~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);

  2168     val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);

  2169        (*if*) p_ = Pos.Met (*then*);

  2170     val (i_model, m_patt) = (met,

  2171            (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)

  2173 val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =

  2174       (*case*)

  2175    I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);

  2176 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =

  2177   (ctxt, m_field, oris, i_model, m_patt, ct);

  2178 (*.NEW*)      val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);

  2179 (*.NEW*)   val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);

  2181 val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =

  2182           (*case*)

  2183        O_Model.contains ctxt m_field o_model t (*of*);

  2184 "~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);

  2185     val ots = ((distinct op =) o flat o (map #5)) ori

  2186     val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots

  2187     val (d, ts) = Input_Descript.split t

  2188     val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);

  2189     (*if*) (subtract op = oids ids) <> [] (*else*);

  2190 	    (*if*) d = TermC.empty (*else*);

  2191 	      (*if*) member op = (map #4 ori) d (*then*);

  2193                 associate_input ctxt sel (d, ts) ori;

  2194 "~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =

  2195   (ctxt, sel, (d, ts), ori);

  2197 (*/------------------- check within associate_input ------------------------------------------\*)

  2198 (*+*)val Add_Given "FunktionsVariable x" = tac;

  2199 (*+*)m_field = "#Given";

  2200 (*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;

  2201 (*+*)val [Free ("x", _)] = vals;

  2202 (*+*)O_Model.to_string @{context} ori = "[\n" ^

  2203   "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

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

  2205   "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  2206   "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  2207   "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  2208   "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  2209   "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";

  2210 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori

  2211 (*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =

  2212   (id, vat, m_field', descript', vals')

  2213 (*\------------------- check within associate_input ----------------------------------------/*)

  2214 \<close> ML \<open>(*\\------------ step into Step.by_tactic -------------------------------------------//*)

  2215 (*\\------------------ step into Step.by_tactic -------------------------------------------//*)

  2216 \<close> ML \<open>(*\------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2-------//*)

  2217 (*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2-------//*)

  2218 (*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2

  2219                                                  val Add_Given "FunktionsVariable x" =  nxt;

  2221 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt

  2222 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt

  2223 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt

  2224 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c]" = nxt

  2225 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2]" = nxt

  2226 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3]" = nxt

  2227 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = nxt

  2228 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

  2230 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt

  2231 (*/------------------- check entry to me Model_Problem -------------------------------------\*)

  2232 (*+*)val ([1], Pbl) = p;

  2233 (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =

  2234   get_obj g_origin pt (fst p);

  2235 (*+*)if O_Model.to_string @{context} o_model = "[\n" ^

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

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

  2238   "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"

  2239 (*

  2240 .. here the O_Model does NOT know, which MethodC will be chosen,

  2241 so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,

  2242 "b_b" and "id_abl" are NOT missing.

  2243 *)

  2244 then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";

  2245 (*\------------------- check entry to me Model_Problem -------------------------------------/*)

  2247 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)

  2248 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)

  2249 \<close> ML \<open>

  2250 \<close> ML \<open>(*ERROR isalist2list applied to NON-list: funs'''*)

  2251 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

  2252 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)

  2254 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)

  2255 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)

  2256 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)

  2258 (*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)

  2259 (*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)

  2260 (*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;

  2261 (*+*)(* by \<up> \<up> \<up> \<up>   "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)

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

  2265   val ("ok", ([], [], (_, _))) = (*case*)

  2266       Step.by_tactic tac (pt, p) (*of*);

  2267 "~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  2268   val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);

  2269 	    (*if*) Tactic.for_specify' tac' (*then*);

  2271   val ("ok", ([], [], (_, _))) =

  2272 Step_Specify.by_tactic tac' ptp;

  2273 (*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)

  2274 (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =

  2275   get_obj g_origin pt (fst p);

  2276 (*+*)if O_Model.to_string ctxt o_model = "[\n" ^

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

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

  2279   "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"

  2280 (*

  2281 .. here the MethodC has been determined by the user,

  2282 so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,

  2283 "b_b" and "id_abl" WOULD BE missing (added by O_Model.).

  2284 *)

  2285 then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";

  2286 (*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)

  2287 "~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =

  2288   (tac', ptp);

  2289 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,

  2290 (*.NEW*)    ...} =Calc.specify_data (pt, pos);

  2291 (*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;

  2292 (*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

  2293 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))

  2294 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);

  2296 (*/------------------- check for entry to O_Model.complete_for -----------------------------\*)

  2297 (*+*)if mID = ["Biegelinien", "ausBelastung"]

  2298 (*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";

  2299 (*+*)if Model_Pattern.to_string ctxt m_patt = "[\"" ^

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

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

  2302   "(#Given, (Biegelinie, b_b))\", \"" ^

  2303   "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^

  2304   "(#Given, (Biegemoment, id_momentum))\", \"" ^

  2305   "(#Given, (Querkraft, id_lat_force))\", \"" ^

  2306   "(#Find, (Funktionen, fun_s))\"]"

  2307 (*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";

  2308 (*+*)if O_Model.to_string ctxt o_model = "[\n" ^

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

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

  2311   "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"

  2312 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";

  2313 (*+*) O_Model.to_string ctxt root_model;

  2314 (*+*) O_Model.to_string ctxt o_model';

  2315   "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";

  2316 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)

  2318   O_Model.complete_for m_patt root_model (o_model, ctxt);

  2319 "~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =

  2320   (m_patt, root_model, (o_model, ctxt));

  2321     val  missing = m_patt |> filter_out

  2322       (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))

  2323 ;

  2324     val add = root_model

  2325       |> filter

  2326         (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)

  2327 ;

  2328     (o_model @ add

  2329 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

  2330 (*NEW*)

  2331       |> map (fn (_, b, c, d, e) => (b, c, d, e))

  2332       |> add_enumerate

  2333       |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),

  2334     ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);

  2335 "~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =

  2336   ((o_model @ add)

  2337 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

  2338 (*NEW*)

  2339       |> map (fn (_, b, c, d, e) => (b, c, d, e))

  2340       |> add_enumerate

  2341       |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),

  2342     ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));

  2344 (*/------------------- check within O_Model.complete_for -------------------------------------------\*)

  2345 (*+*) O_Model.to_string ctxt o_model';

  2346   "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";

  2347 (*\------------------- check within O_Model.complete_for -------------------------------------------/*)

  2349 (*.NEW*) val thy = ThyC.get_theory ctxt dI

  2350 (*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';

  2351 (*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))

  2352 (*.NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)

  2353 ;

  2354 (*+*) I_Model.to_string ctxt i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";

  2355 (*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =

  2356 (*+*)  Calc.specify_data (pt, pos);

  2357 (*+*)pos = ([1], Met);

  2359          ("ok", ([], [], (pt, pos)))  (*return from Step_Specify.by_tactic*);

  2360 "~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =

  2361          ("ok", ([], [], (pt, pos)));

  2362 (*  val ("helpless", ([(xxxxx, _, _)], _, _)) =  (*case*)*)

  2363   (*  SHOULD BE    \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)

  2365 val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =

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

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

  2368 (*.NEW*)(*if*) on_calc_end ip (*else*);

  2369 (*.NEW*)    val (_, probl_id, _) = Calc.references (pt, p);

  2370 (*-"-*)    val _ = (*case*)  tacis (*of*);

  2371 (*.NEW*)      (*if*) probl_id = Problem.id_empty (*else*);

  2373 (*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =

  2374          switch_specify_solve p_ (pt, ip);

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

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

  2378   val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =

  2379           specify_do_next (pt, input_pos);

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

  2382     val (_, (p_', tac)) =

  2383    Specify.find_next_step ptp;

  2384 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

  2385     val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

  2386       spec = refs, ...} = Calc.specify_data (pt, pos);

  2387     val ctxt = Ctree.get_ctxt pt pos

  2388 ;

  2389 (*+*)O_Model.to_string ctxt oris = "[\n" ^

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

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

  2392   "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  2393   "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  2394   "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";

  2395 (*+*)val (true, []) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST pbl) (Pos.Met, mI');

  2396 (*+*)I_Model.to_string ctxt met = "[\n" ^

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

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

  2399   "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  2400   "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^

  2401   "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";

  2403     (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

  2404       (*if*) p_ = Pos.Pbl (*else*);

  2405 val return = for_method ctxt oris (o_refs, refs) (pbl, met);

  2406 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);

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

  2409     val Add_Given "Biegelinie y" = (*case*) tac (*of*);

  2410 val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));

  2411 (*+*)val Add_Given "Biegelinie y" = tac;

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

  2413     val _ = (*case*) tac (*of*);

  2415   val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =

  2416 Step_Specify.by_tactic_input tac (pt, (p, p_'))

  2417 (*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)

  2418 (*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));

  2419 (*+*)I_Model.to_string ctxt meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)

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

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

  2422   "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  2423   "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^

  2424   "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";

  2425 (*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)

  2426 "~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =   (tac, (pt, (p, p_')));

  2428    Specify.by_Add_ "#Given" ct ptp;

  2429 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);

  2430     val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);

  2431        (*if*) p_ = Pos.Met (*then*);

  2432     val (i_model, m_patt) = (met,

  2433            (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)

  2434 val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =

  2435       (*case*)

  2436    check_single ctxt m_field oris i_model m_patt ct (*of*);

  2438 (*/------------------- check for entry to check_single -------------------------------------\*)

  2439 (*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";

  2440 (*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";

  2441 (*\------------------- check for entry to check_single -------------------------------------/*)

  2443 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =

  2444   (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);

  2445       val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);

  2447 (*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;

  2448 (*("associate_input: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)

  2450           (*case*)

  2451    contains ctxt m_field o_model t (*of*);

  2452 "~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);

  2453     val ots = ((distinct op =) o flat o (map #5)) ori

  2454     val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots

  2455     val (d, ts) = Input_Descript.split t

  2456     val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);

  2457     (*if*) (subtract op = oids ids) <> [] (*else*);

  2458 	    (*if*) d = TermC.empty (*else*);

  2459 	      (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);

  2461   (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);

  2462 "~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);

  2464 (*+/---------------- bypass recursion of associate_input' ----------------\*)

  2465 (*+*)O_Model.to_string ctxt oris = "[\n" ^

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

  2467   "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  2468   "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  2469   "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";

  2470 (*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)

  2471 (*+\---------------- bypass recursion of associate_input' ----------------/*)

  2473     (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);

  2475 (*/------------------- check within associate_input' -------------------------------\*)

  2476 (*+*)if sel = "#Given" andalso sel' = "#Given"

  2477 (*+*)then () else error "associate_input' Model_Pattern CHANGED";

  2478 (*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)

  2479 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

  2480 (*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^

  2481   "(#Given, (Streckenlast, q_q))\", \"" ^

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

  2483   "(#Find, (Funktionen, funs'''))\"]"

  2484 (*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";

  2485 (* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)

  2486 (*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^

  2487   "(#Given, (Traegerlaenge, l_l))\", \"" ^

  2488   "(#Given, (Streckenlast, q_q))\", \"" ^

  2489   "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)

  2490   "(#Relate, (Randbedingungen, r_b))\"]"

  2491 (*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";

  2492 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

  2493 (*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^

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

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

  2496   "(#Given, (Biegelinie, b_b))\", \"" ^

  2497   "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^

  2498   "(#Given, (Biegemoment, id_momentum))\", \"" ^

  2499   "(#Given, (Querkraft, id_lat_force))\", \"" ^

  2500   "(#Find, (Funktionen, fun_s))\"]"

  2501 (*+*)then () else error "associate_input' Model_Pattern CHANGED";

  2502 (*+*)if UnparseC.term ctxt d = "Biegelinie" andalso UnparseC.terms ctxt ts = "[y]"

  2503 (*+*)  andalso UnparseC.terms ctxt ts' = "[y]"

  2504 (*+*)then

  2505 (*+*)  (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()

  2506 (*+*)  | _ => error "check within associate_input' CHANGED 1")

  2507 (*+*)else error "check within associate_input' CHANGED 2";

  2508 (*\------------------- check within associate_input' -------------------------------/*)

  2510 (*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)

  2511 (*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)

  2512 (*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;

  2513                                                      val Add_Given "Biegelinie y" = nxt

  2515 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt

  2516 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt

  2517 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt

  2518 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt

  2520 (*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt

  2521 (*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt

  2522 (*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt

  2523 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt

  2524 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt

  2525 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt

  2526 ;

  2527 (*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)

  2528 if p = ([1, 3], Pbl) andalso

  2529   f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],

  2530     Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],

  2531     Relate = [], Where = [], With = []})

  2532 then

  2533   (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")

  2534 else error "specify-phase: low level CHANGED 2";

  2535 (*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)

  2536 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

  2539 \<close> ML \<open>

  2540 \<close>

  2542 section \<open>===================================================================================\<close>

  2543 section \<open>=====   ===========================================================================\<close>

  2544 ML \<open>

  2545 \<close> ML \<open>

  2547 \<close> ML \<open>

  2548 \<close>

  2549 end

author	wneuper <Walther.Neuper@jku.at>
	Mon, 20 Nov 2023 10:49:54 +0100
changeset 60765	5e91c279af3a
parent 60763	2121f1a39a64
child 60766	2e0603ca18a4
permissions	-rw-r--r--