wneuper/isa: test/Tools/isac/Knowledge/eqsystem.sml@a3ce4017f41d

     1 (* tests on systems of equations

     2    author: Walther Neuper

     3    050826,

     4    (c) due to copyright terms

     6 use"../smltest/IsacKnowledge/eqsystem.sml";

     7 use"eqsystem.sml";

     8 *)

    10 "-----------------------------------------------------------------";

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

    12 "-----------------------------------------------------------------";

    13 "----------- occur_exactly_in ------------------------------------";

    14 "----------- problems --------------------------------------------";

    15 "----------- rewrite-order ord_simplify_System -------------------";

    16 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";

    17 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";

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

    19 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";

    20 "----------- script [EqSystem,normalize,2x2] ---------------------";

    21 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";

    22 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";

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

    24 "----------- refine [2x2,linear,system] search error--------------";

    25 "----------- me [EqSystem,normalize,2x2] -------------------------";

    26 "----------- me [linear,system] ..normalize..top_down_sub..-------";

    27 "----------- all systems from Biegelinie -------------------------";

    28 "----------- 4x4 systems from Biegelinie -------------------------";

    29 "-----------------------------------------------------------------";

    30 "-----------------------------------------------------------------";

    31 "-----------------------------------------------------------------";

    33 (*=== inhibit exn ?=============================================================

    34 val thy = EqSystem.thy;

    36 "----------- occur_exactly_in ------------------------------------";

    37 "----------- occur_exactly_in ------------------------------------";

    38 "----------- occur_exactly_in ------------------------------------";

    39 val all = [str2term"c", str2term"c_2", str2term"c_3"];

    40 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    42 if occur_exactly_in [str2term"c", str2term"c_2"] all t

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

    45 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)

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

    48 if not (occur_exactly_in [str2term"c_2"] all t)

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

    52 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \

    53 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    54 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;

    55 if str = "[c, c_2] from_ [c, c_2,\n                c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()

    56 else error "eval_occur_exactly_in [c, c_2]";

    58 val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \

    59 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    60 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;

    61 if str = "[c, c_2,\n c_3] from_ [c, c_2,\n             c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()

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

    64 val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \

    65 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    66 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;

    67 if str = "[c_2] from_ [c, c_2,\n             c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()

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

    70 val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";

    71 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;

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

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

    75 val t =

    76     str2term

    77 	"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";

    78 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;

    79 if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \

    80 	 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()

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

    84 "----------- problems --------------------------------------------";

    85 "----------- problems --------------------------------------------";

    86 "----------- problems --------------------------------------------";

    87 val t = str2term "length_ [x+y=1,y=2] = 2";

    88 atomty t;

    89 val testrls = append_rls "testrls" e_rls

    90 			 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),

    91 			  (Thm ("length_Cons_",num_str @{thm length_Cons_})),

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

    93 			  Calc ("HOL.eq",eval_equal "#equal_")

    94 			  ];

    95 val SOME (t',_) = rewrite_set_ thy false testrls t;

    96 if term2str t' = "HOL.True" then ()

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

    99 val SOME t = parse EqSystem.thy "solution L";

   100 atomty (term_of t);

   101 val SOME t = parse Biegelinie.thy "solution L";

   102 atomty (term_of t);

   104 val t = str2term

   105 "(tl (tl (tl v_s))) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))";

   106 atomty t;

   107 val t = str2term

   108 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \

   109 \(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";

   110 val SOME (t,_) =

   111     rewrite_set_ thy true

   112 		 (append_rls "prls_" e_rls

   113 			     [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),

   114 			      Thm ("nth_Nil_",num_str @{thm nth_Nil_}),

   115 			      Thm ("tl_Cons",num_str @{thm tl_Cons}),

   116 			      Thm ("tl_Nil",num_str @{thm tl_Nil}),

   117 			      Calc ("EqSystem.occur'_exactly'_in",

   118 				    eval_occur_exactly_in

   119 					"#eval_occur_exactly_in_")

   120 			      ]) t;

   121 if t = HOLogic.true_const then ()

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

   125 "----------- rewrite-order ord_simplify_System -------------------";

   126 "----------- rewrite-order ord_simplify_System -------------------";

   127 "----------- rewrite-order ord_simplify_System -------------------";

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

   129 "--- add_commute ---";

   130 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",

   131 				       str2term"c * x") then ()

   132 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";

   134 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",

   135 				       str2term"c_2") then ()

   136 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";

   138 if ord_simplify_System false thy [] (str2term"c * x",

   139 				       str2term"c_2") then ()

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

   142 "--- mult_commute ---";

   143 if ord_simplify_System false thy [] (str2term"x * c",

   144 				       str2term"c * x") then ()

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

   147 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",

   148 				       str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")

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

   151 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",

   152 				       str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")

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

   156 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";

   157 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";

   158 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";

   159 val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\

   160 	        \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";

   161 val bdvs = [(str2term"bdv_1",str2term"c"),

   162 	    (str2term"bdv_2",str2term"c_2")];

   163 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

   164 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"

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

   167 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

   168 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"

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

   171 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;

   172 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"

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

   175 val SOME (t,_) = rewrite_set_ thy true order_system t;

   176 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"

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

   180 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";

   181 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";

   182 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";

   183 val thy = (theory "Isac") (*because of Undeclared constant "Biegelinie.EI*);

   184 val t =

   185     str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 +         \

   186 	    \                                     -1 * q_0 / 24 * 0 ^^^ 4),\

   187 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +         \

   188 	    \                                     -1 * q_0 / 24 * L ^^^ 4)]";

   189 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;

   190 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"

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

   193 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

   194 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"

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

   197 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

   198 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"

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

   201 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;

   202 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"

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

   205 val xxx = rewrite_set_ thy true order_system t;

   206 if is_none xxx

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

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

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

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

   213 val e1__ = str2term "c_2 = 77";

   214 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";

   215 val bdvs = [(str2term"bdv_1",str2term"c"),

   216 	    (str2term"bdv_2",str2term"c_2")];

   217 val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;

   218 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()

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

   221 val SOME (e2__,_) =

   222     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;

   223 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()

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

   226 val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;

   227 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()

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

   230 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";

   231 val SOME (t,_) = rewrite_set_ thy true order_system t;

   232 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()

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

   235 if not (ord_simplify_System

   236 	    false thy []

   237 	    (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",

   238 	     str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))

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

   241 trace_rewrite:=true;

   242 trace_rewrite:=false;

   245 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";

   246 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";

   247 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";

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

   249 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\

   250 	        \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\

   251 		\c + c_2 + c_3 + c_4 = 0,\

   252 		\c_2 + c_3 + c_4 = 0]";

   253 val bdvs = [(str2term"bdv_1",str2term"c"),

   254 	    (str2term"bdv_2",str2term"c_2"),

   255 	    (str2term"bdv_3",str2term"c_3"),

   256 	    (str2term"bdv_4",str2term"c_4")];

   257 val SOME (t,_) =

   258     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

   259 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\

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

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

   263 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

   264 if term2str t = "[c_4 = 0, \

   265 	        \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \

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

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

   269 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

   270 if term2str t = "[c_4 = 0,\

   271 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\

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

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

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

   276 val SOME (t,_) = rewrite_set_ thy true order_system t;

   277 if term2str t = "[c_4 = 0,\

   278 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\

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

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

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

   284 "----------- script [EqSystem,normalize,2x2] ---------------------";

   285 "----------- script [EqSystem,normalize,2x2] ---------------------";

   286 "----------- script [EqSystem,normalize,2x2] ---------------------";

   287 val str =

   288 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   289 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   290 \                                simplify_System_parenthesized False) es_  \

   291 \   in ([]))";

   292 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   293 val str =

   294 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   295 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   296 \                                 simplify_System_parenthesized False) es_  \

   297 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   298 \                  []))";

   299 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   300 val str =

   301 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   302 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   303 \                                 simplify_System_parenthesized False) es_  \

   304 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   305 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   306 ;

   307 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   308 val str =

   309 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   310 \  (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   311 \                                 simplify_System_parenthesized False) es_  \

   312 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   313 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   314 ;

   315 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   316 val str =

   317 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   318 \  (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   319 \                                 simplify_System_parenthesized False)) es_  \

   320 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   321 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   322 ;

   323 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   324 val str =

   325 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   326 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   327 \                                 simplify_System_parenthesized False)) @@\

   328 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   329 \                                 simplify_System_parenthesized False))) es_\

   330 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   331 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   332 ;

   333 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   334 val str =

   335 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   336 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   337 \                                 simplify_System_parenthesized False)) @@\

   338 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   339 \                                 simplify_System_parenthesized False)) @@\

   340 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   341 \                                 simplify_System_parenthesized False))) es_\

   342 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   343 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   344 ;

   345 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   346 val str =

   347 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   348 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   349 \                                 simplify_System_parenthesized False)) @@\

   350 \               (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\

   351 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   352 \                                 simplify_System_parenthesized False)) @@\

   353 \               (Try (Rewrite_Set order_system False))) es_\

   354 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   355 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   356 ;

   357 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   358 val str =

   359 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   360 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   361 \                                 simplify_System_parenthesized False)) @@\

   362 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\

   363 \                                                    isolate_bdvs False)) @@\

   364 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   365 \                                 simplify_System_parenthesized False)) @@\

   366 \               (Try (Rewrite_Set order_system False))) es_\

   367 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   368 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   369 ;

   370 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   371 val str =

   372 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   373 \  (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\

   374 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   375 \                                                    isolate_bdvs False)) @@\

   376 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   377 \                                 simplify_System_parenthesized False)) @@\

   378 \               (Try (Rewrite_Set order_system False))) es_\

   379 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

   380 \                  [BOOL_LIST es__, REAL_LIST v_s]))"

   381 ;

   382 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   383 (*---^^^-OK-----------------------------------------------------------------*)

   384 (*---vvv-NOT ok-------------------------------------------------------------*)

   387 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";

   388 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";

   389 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";

   390 val str =

   391 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   392 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   393 \                                 simplify_System_parenthesized False) es_  \

   394 \   in ([]))";

   395 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   396 val str =

   397 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   398 \  (let e1__ = Take (hd es_)                \

   399 \   in ([]))";

   400 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   401 val str =

   402 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   403 \  (let e1__ = Take (hd es_);               \

   404 \       e1__ = Take (hd es_)                \

   405 \   in ([]))";

   406 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   407 val str =

   408 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   409 \  (let e1__ = Take (hd es_);               \

   410 \       e1__ = (Take (hd es_))\

   411 \   in ([]))";

   412 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   413 val str =

   414 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   415 \  (let e1__ = Take (hd es_);               \

   416 \       e1__ = ((Rewrite_Set order_system False)) e1__\

   417 \   in ([]))";

   418 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   419 (*--------------------------------------------------------------------------*)

   420 val str =

   421 "(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   422 \                                           isolate_bdvs False) (e1__::bool)";

   423 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   424 (*--------------------------------------------------------------------------*)

   425 val str =

   426 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   427 \  (let e1__ = Take (hd es_);               \

   428 \       e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   429 \                                           isolate_bdvs False)) e1__\

   430 \   in ([]))";

   431 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   432 val str =

   433 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   434 \  (let e1__ = Take (hd es_);               \

   435 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   436 \                                           isolate_bdvs False)) @@\

   437 \               (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   438 \                                 simplify_System False)) e1__\

   439 \   in ([]))";

   440 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   441 val str =

   442 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   443 \  (let e1__ = Take (hd es_);               \

   444 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   445 \                                           isolate_bdvs False)) @@\

   446 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   447 \                                 simplify_System False))) e1__\

   448 \   in ([]))";

   449 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   450 val str =

   451 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   452 \  (let e1__ = Take (hd es_);                                                \

   453 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   454 \                                           isolate_bdvs False)) @@          \

   455 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   456 \                                 simplify_System False))) e1__;           \

   457 \       e2__ = Take (hd (tl es_))                                            \

   458 \   in ([]))";

   459 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   460 val str =

   461 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   462 \  (let e1__ = Take (hd es_);                                                \

   463 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   464 \                                           isolate_bdvs False)) @@          \

   465 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   466 \                                 simplify_System False))) e1__;           \

   467 \       e2__ = Take (hd (tl es_));                                           \

   468 \       e2__ = Substitute [e1__] e2__                                       \

   469 \   in ([]))";

   470 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   471 val str =

   472 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   473 \  (let e1__ = Take (hd es_);                                                \

   474 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   475 \                                           isolate_bdvs False)) @@          \

   476 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   477 \                                 simplify_System False))) e1__;           \

   478 \       e2__ = Take (hd (tl es_));                                           \

   479 \       e2__ = ((Substitute [e1__])) e2__                                  \

   480 \   in ([]))";

   481 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   482 val str =

   483 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   484 \  (let e1__ = Take (hd es_);                                                \

   485 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   486 \                                      isolate_bdvs False)) @@               \

   487 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   488 \                                 simplify_System False))) e1__;           \

   489 \       e2__ = Take (hd (tl es_));                                           \

   490 \       e2__ = ((Substitute [e1__]) @@                                       \

   491 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   492 \                                      isolate_bdvs False)) @@               \

   493 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   494 \                                 simplify_System False))) e2__            \

   495 \   in [e1__, e2__])"

   496 ;

   497 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   498 val str =

   499 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   500 \  (let e1__ = Take (hd es_);                                                \

   501 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   502 \                                      isolate_bdvs False)) @@               \

   503 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   504 \                                 simplify_System False))) e1__;           \

   505 \       e2__ = Take (hd (tl es_));                                           \

   506 \       e2__ = ((Substitute [e1__]) @@                                       \

   507 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   508 \                                 simplify_System_parenthesized False)) @@ \

   509 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   510 \                                      isolate_bdvs False)) @@               \

   511 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   512 \                                 simplify_System False)) @@               \

   513 \               (Try (Rewrite_Set order_system False))) e2__                 \

   514 \   in [e1__, e2__])"

   515 ;

   516 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   517 (*---^^^-OK-----------------------------------------------------------------*)

   518 val str =

   519 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

   520 \  (let e1__ = Take (hd es_);                                                \

   521 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   522 \                                      isolate_bdvs False)) @@               \

   523 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   524 \                                 simplify_System False))) e1__;           \

   525 \       e2__ = Take (hd (tl es_));                                           \

   526 \       e2__ = ((Substitute [e1__]) @@                                       \

   527 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   528 \                                 simplify_System_parenthesized False)) @@ \

   529 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   530 \                                      isolate_bdvs False)) @@               \

   531 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   532 \                                 simplify_System False))) e2__;           \

   533 \       es__ = Take [e1__, e2__]\

   534 \   in (Try (Rewrite_Set order_system False)) es__)"

   535 ;

   536 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   537 (*---vvv-NOT ok-------------------------------------------------------------*)

   538 atomty sc;

   540 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";

   541 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";

   542 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";

   543 val str =

   544 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   545 \  (let es__ = Take es_;   \

   546 \       e1__ = hd es__\

   547 \   in ([]))"

   548 ;

   549 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   550 val str =

   551 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   552 \  (let es__ = Take es_;   \

   553 \       e1__ = hd es__;    \

   554 \       e2__ = hd (tl es__)\

   555 \   in ([]))"

   556 ;

   557 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   558 val str =

   559 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   560 \  (let es__ = Take es_;   \

   561 \       e1__ = hd es__;    \

   562 \       e2__ = hd (tl es__);\

   563 \       es__ = [1=2,3=4]\

   564 \   in ([]))"

   565 ;

   566 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   567 val str =

   568 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   569 \  (let es__ = Take es_;   \

   570 \       e1__ = hd es__;    \

   571 \       e2__ = hd (tl es__);\

   572 \       es__ = [e1__,e2__]\

   573 \   in ([]))"

   574 ;

   575 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   576 val str =

   577 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   578 \  (let es__ = Take es_;   \

   579 \       e1__ = hd es__;    \

   580 \       e2__ = hd (tl es__);\

   581 \       es__ = [e1__, Substitute [e1__] e2__];\

   582 \       es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   583 \                                 simplify_System False)) es__            \

   584 \   in ([]))"

   585 ;

   586 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   587 val str =

   588 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   589 \  (let es__ = Take es_;   \

   590 \       e1__ = hd es__;    \

   591 \       e2__ = hd (tl es__);\

   592 \       es__ = [e1__, Substitute [e1__] e2__];\

   593 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   594 \                                      isolate_bdvs False)) @@               \

   595 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   596 \                                 simplify_System False))) es__            \

   597 \   in ([]))"

   598 ;

   599 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   600 val str =

   601 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   602 \  (let es__ = Take es_;   \

   603 \       e1__ = hd es__;    \

   604 \       e2__ = hd (tl es__);\

   605 \       es__ = [e1__, Substitute [e1__] e2__];\

   606 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   607 \                                 simplify_System_parenthesized False)) @@  \

   608 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   609 \                                      isolate_bdvs False)) @@               \

   610 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   611 \                                 simplify_System False))) es__            \

   612 \   in ([]))"

   613 ;

   614 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   615 val str =

   616 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \

   617 \  (let es__ = Take es_;                                                     \

   618 \       e1__ = hd es__;                                                      \

   619 \       e2__ = hd (tl es__);                                                 \

   620 \       es__ = [e1__, Substitute [e1__] e2__];                               \

   621 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   622 \                                 simplify_System_parenthesized False)) @@  \

   623 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   624 \                                      isolate_bdvs False))              @@  \

   625 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   626 \                                 simplify_System False))) es__            \

   627 \   in es__)"

   628 ;

   629 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   630 val str =

   631 "Script SolveSystemScript (es_::bool list) (v_s::real list) =         \

   632 \  (let es__ = Take es_;                                              \

   633 \       e1__ = hd es__;                                               \

   634 \       e2__ = hd (tl es__);                                          \

   635 \       es__ = [e1__, Substitute [e1__] e2__]                         \

   636 \   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   637 \                                 simplify_System_parenthesized False)) @@   \

   638 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \

   639 \                              isolate_bdvs False))              @@   \

   640 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   641 \                                 simplify_System False))) es__)"

   642 ;

   643 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   644 (*---^^^-OK-----------------------------------------------------------------*)

   645 val str =

   646 "Script SolveSystemScript (es_::bool list) (v_s::real list) =         \

   647 \  (let es__ = Take es_;                                              \

   648 \       e1__ = hd es__;                                               \

   649 \       e2__ = hd (tl es__);                                          \

   650 \       es__ = [e1__, Substitute [e1__] e2__]                         "^

   651 (* this        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'

   652    which is not yet searched for 'STac's; thus this script does not yet work*)

   653 "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   654 \                                 simplify_System_parenthesized False)) @@   \

   655 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \

   656 \                              isolate_bdvs False))              @@   \

   657 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

   658 \                                 simplify_System False))) es__)"

   659 ;

   660 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   661 (*---vvv-NOT ok-------------------------------------------------------------*)

   662 atomty sc;

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

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

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

   668 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\

   669 	               \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",

   670 	   "solveForVars [c, c_2]", "solution L"];

   671 val matches = refine fmz ["linear","system"];

   672 case matches of [_,_,_,

   673 		 Matches (["normalize", "2x2", "linear", "system"],

   674 			  {Find = [Correct "solution L"],

   675 			   With = [],

   676 			   Given =

   677 			   [Correct

   678 				"equalities\n [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\n  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",

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

   680 			   Where = [],

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

   682 	      | _ => error "eqsystem.sml refine ['normalize','2x2'...]";

   685 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",

   686 	   "solveForVars [c, c_2]", "solution L"];

   687 val matches = refine fmz ["linear","system"];

   688 case matches of [_,_,

   689 		 Matches

   690 		     (["triangular", "2x2", "linear", "system"],

   691 		      {Find = [Correct "solution L"],

   692 		       With = [],

   693 		       Given =

   694 		       [Correct

   695 			    "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",

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

   697 		       Where =

   698 		       [Correct

   699 			    "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1\n       [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",

   700 			    Correct

   701 				"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"],

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

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

   706 (*WN051014----------------------------------------------------------------

   707   the above 'val matches = refine fmz ["linear","system"]'

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

   709 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",

   710 	   "solveForVars [c, c_2]", "solution L"];

   711 val matches = refine fmz ["triangular", "2x2", "linear","system"];

   712 (*... resulted in

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

   714           [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)

   716 val t = str2term"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\

   717 		\[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]";

   718 trace_rewrite:=true;

   719 val SOME (t',_) = rewrite_set_ thy false prls_triangular t;

   720 (*found:...

   721 ##  try thm: nth_Cons_

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

   723 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =

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

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

   726 #####  try calc: op <'

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

   729 ... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)

   730 trace_rewrite:=false;

   731 (*WN051014------------------------------------------------------------------*)

   733 "----- relaxed preconditions for triangular system";

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

   735 	   \            0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\

   736 	   \            0 = c_4,                           \

   737 	   \            0 = c_3]",

   738 	   "solveForVars [c, c_2, c_3, c_4]", "solution L"];

   739 val matches = refine fmz ["linear","system"];

   740 (* trace_rewrite := true;

   741    trace_rewrite := false;

   742    *)

   743 (*print_depth 6; matches; print_depth 3;*)

   744 case matches of

   745     [Matches (["linear", "system"], _),

   746      NoMatch (["2x2", "linear", "system"], _),

   747      NoMatch (["3x3", "linear", "system"], _),

   748      Matches (["4x4", "linear", "system"], _),

   749      NoMatch (["triangular", "4x4", "linear", "system"], _),

   750      Matches (["normalize", "4x4", "linear", "system"], _)] => ()

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

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

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

   755 	   \            0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\

   756 	   \            0 = c_3,                           \

   757 	   \            0 = c_4]",

   758 	   "solveForVars [c, c_2, c_3, c_4]", "solution L"];

   759 val matches = refine fmz ["triangular", "4x4", "linear","system"];

   760 (* print_depth 11; matches; print_depth 3;

   761    *)

   762 case matches of

   763     [Matches (["triangular", "4x4", "linear", "system"], _)] => ()

   764   | _ => error "eqsystem.sml: refine relaxed triangular sys Matches";

   765 val matches = refine fmz ["linear","system"];

   768 "----------- refine [2x2,linear,system] search error--------------";

   769 "----------- refine [2x2,linear,system] search error--------------";

   770 "----------- refine [2x2,linear,system] search error--------------";

   771 (*didn't go into ["2x2", "linear", "system"];

   772   we investigated in these steps:*)

   773 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\

   774 	               \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",

   775 	   "solveForVars [c, c_2]", "solution L"];

   776 trace_rewrite:=true;

   777 val matches = refine fmz ["2x2", "linear","system"];

   778 trace_rewrite:=false;

   779 print_depth 11; matches; print_depth 3;

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

   782 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =

   783 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =

   784        (rev ["linear","system"], fmz, [(*match list*)],

   785 	((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));

   786    *)

   787 > show_types:=true; term2str (hd where_); show_types:=false;

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

   790 =========================================================================\

   791 -------fun prep_pbt

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

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

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

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

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

   797 			],

   798 		       append_rls "e_rls" e_rls [(*for preds in where_*)],

   799 		       SOME "solveSystem es_ v_s",

   800 		       []));

   801    *)

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

   803 val equalities_es_ = "equalities es_" : string

   804 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;

   805 > show_types:=true; term2str ii; show_types:=false;

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

   807 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   809 > val {where_,...} = get_pbt ["2x2", "linear","system"];

   810 > show_types:=true; term2str (hd where_); show_types:=false;

   812 =========================================================================/

   816 -----fun refin' ff:

   817 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;

   818 [

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

   820  [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

   821   0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

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

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

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

   826 > (writeln o pres2str) pre';

   827 [

   828 (false, length_ es_ = 2),

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

   831 ----- fun match_oris':

   832 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;

   833 > (writeln o pres2str) pre';

   834 ..as in refin'

   836 ----- fun check_preconds'

   837 > (writeln o env2str) env;

   838 ["

   839 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

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

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

   842 (ss___, L)"]

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

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

   847 > val pre1 = hd pres;

   848 atomty pre1;

   849 ***

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

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

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

   853 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~

   854 *** . Free (2, real)

   855 ***

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

   858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   859 *)

   862 "----------- me [EqSystem,normalize,2x2] -------------------------";

   863 "----------- me [EqSystem,normalize,2x2] -------------------------";

   864 "----------- me [EqSystem,normalize,2x2] -------------------------";

   865 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\

   866 	               \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",

   867 	   "solveForVars [c, c_2]", "solution L"];

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

   869   ("Biegelinie",["normalize", "2x2", "linear", "system"],

   870    ["EqSystem","normalize","2x2"]);

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

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

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

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

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

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

   877 case nxt of ("Specify_Method",_) => ()

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

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

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

   882 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);

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

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

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

   886 case nxt of

   887     (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()

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

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

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

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

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

   894 case nxt of

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

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

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

   899 val PblObj {probl,...} = get_obj I pt [5];

   900     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;

   901 (*[

   902 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),

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

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

   905 *)

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

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

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

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

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

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

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

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

   914 case nxt of

   915     (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()

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

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

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

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

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

   921 case nxt of

   922     (_, End_Proof') => ()

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

   926 "----------- me [linear,system] ..normalize..top_down_sub..-------";

   927 "----------- me [linear,system] ..normalize..top_down_sub..-------";

   928 "----------- me [linear,system] ..normalize..top_down_sub..-------";

   929 val fmz =

   930     ["equalities\

   931      \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 +                \

   932      \                                            -1 * q_0 / 24 * 0 ^^^ 4),\

   933      \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +                \

   934      \                                            -1 * q_0 / 24 * L ^^^ 4)]",

   935      "solveForVars [c, c_2]", "solution L"];

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

   937   ("Biegelinie",["linear", "system"], ["no_met"]);

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

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

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

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

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

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

   944 case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()

   945 	  | _ => error "eqsystem.sml [linear,system] specify b";

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

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

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

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

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

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

   952 if f2str f =

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

   954 then () else error "eqsystem.sml me simpl. before SubProblem b";

   955 case nxt of

   956     (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()

   957   | _ => error "eqsystem.sml me [linear,system] SubProblem b";

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

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

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

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

   963 case nxt of

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

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

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

   968 val PblObj {probl,...} = get_obj I pt [5];

   969     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;

   970 (*[

   971 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),

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

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

   974 *)

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

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

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

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

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

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

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

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

   983 case nxt of

   984     (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()

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

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

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

   988 if f2str f =

   989 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"

   990 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";

   991 case nxt of

   992     (_, End_Proof') => ()

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

   996 "----------- all systems from Biegelinie -------------------------";

   997 "----------- all systems from Biegelinie -------------------------";

   998 "----------- all systems from Biegelinie -------------------------";

   999 val subst = [(str2term "bdv_1", str2term "c"),

  1000 	     (str2term "bdv_2", str2term "c_2"),

  1001 	     (str2term "bdv_3", str2term "c_3"),

  1002 	     (str2term "bdv_4", str2term "c_4")];

  1003 "------- Bsp 7.27";

  1004 states:=[];

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

  1006 	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",

  1007 	     "FunktionsVariable x"],

  1008 	    ("Biegelinie", ["Biegelinien"],

  1009 		     ["IntegrierenUndKonstanteBestimmen2"]))];

  1010 moveActiveRoot 1;

  1011 (*

  1012 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1013 ##7.27##          ordered           substs

  1014           c_4       c_2

  1015 c c_2 c_3 c_4     c c_2             1->2: c

  1016   c_2                       c_4

  1017 c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)

  1018 val t = str2term"[0 = c_4,                           \

  1019 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                       \

  1020 \ 0 = c_2,                                           \

  1021 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";

  1022 val SOME (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;

  1023 term2str t';

  1024 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n 0 + -1 * (c_4 + L * c_3),\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]";

  1027 "----- 7.27 go through the rewrites in met_eqsys_norm_4x4";

  1028 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";

  1029 val NONE = rewrite_set_ thy false norm_Rational t;

  1030 val SOME (t,_) =

  1031     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

  1032 term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";

  1033 "--- isolate_bdvs_4x4";

  1034 (*

  1035 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

  1036 term2str t;

  1037 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;

  1038 term2str t;

  1039 val SOME (t,_) = rewrite_set_ thy false order_system t;

  1040 term2str t;

  1041 *)

  1043 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1044 states:=[];

  1045 CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",

  1046 	    "Biegelinie y",

  1047 	    "Randbedingungen [y L = 0, y' L = 0]",

  1048 	    "FunktionsVariable x"],

  1049 	   ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],

  1050 	    ["Biegelinien", "AusMomentenlinie"]))];

  1051 moveActiveRoot 1;

  1052 (*

  1053 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1054 *)

  1056 "------- Bsp 7.69";

  1057 states:=[];

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

  1059 	     "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",

  1060 	     "FunktionsVariable x"],

  1061 	    ("Biegelinie", ["Biegelinien"],

  1062 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1063 moveActiveRoot 1;

  1064 (*

  1065 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1066 ##7.69##          ordered           subst                   2x2

  1067           c_4           c_3

  1068 c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2

  1069       c_3                   c_4

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

  1071 val t = str2term"[0 = c_4 + 0 / (-1 * EI),                                   \

  1072 \ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                                              \

  1073 \ 0 = c_3 + 0 / (-1 * EI),                                                   \

  1074 \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";

  1076 "------- Bsp 7.70";

  1077 states:=[];

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

  1079 	     "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",

  1080 	     "FunktionsVariable x"],

  1081 	    ("Biegelinie", ["Biegelinien"],

  1082 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1083 moveActiveRoot 1;

  1084 (*

  1085 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1086 ##7.70##        |subst

  1087 c		|

  1088 c c_2           |1:c -> 2:c_2

  1089       c_3	|

  1090           c_4   |            STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)

  1092 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";

  1093 val t = str2term"[L * q_0 = c,                       \

  1094 		\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\

  1095 		\ 0 = c_4,                           \

  1096 		\ 0 = c_3]";

  1097 val SOME (t,_) =

  1098     rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;

  1099 val SOME (t,_) =

  1100     rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;

  1101 val SOME (t,_) =

  1102     rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;

  1103 term2str t =

  1104    "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";

  1105 val SOME (t,_) =

  1106     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

  1107 term2str t =

  1108 "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";

  1109 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

  1110 term2str t =

  1111    "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]";

  1112 val SOME (t,_) =

  1113     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

  1115 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";

  1116 val SOME (t,_) = rewrite_set_ thy false order_system t;

  1117 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()

  1118 else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";

  1121 "----- 7.70 with met normalize: ";

  1122 val fmz = ["equalities                                         \

  1123 	    \[L * q_0 = c,                       \

  1124 		\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\

  1125 		\ 0 = c_4,                           \

  1126 		\ 0 = c_3]",

  1127 	    "solveForVars [c, c_2, c_3, c_4]", "solution L"];

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

  1129   ("Biegelinie",["linear", "system"],["no_met"]);

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

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

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

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

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

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

  1136 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()

  1137 	  | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";

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

  1139 "bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";

  1140 (*vvvWN080102 Exception- Match raised

  1141   since assod Rewrite .. Rewrite'_Set

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

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

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

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

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

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

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

  1151 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"

  1152 then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";

  1153 --------------------------------------------------------------------------*)

  1155 "----- 7.70 with met top_down_: ";

  1156 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";

  1157 (*---vvv-this script failed with if ?!?-------------------------------------*)

  1158 val str =

  1159 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \

  1160 \  (let e1_ = hd es_;                                                  \

  1161 \       v1_ = hd v_s;                                                  \

  1162 \       xxx = if lhs e1_ =!= v1_                                       \

  1163 \             then 0=0                                                 \

  1164 \             else let e1_ = Take e1_;                                 \

  1165 \                      e1_ = (Rewrite_Set_Inst [(bdv_1, hd v_s),       \

  1166 \                                               (bdv_2, hd (tl v_s))]  \

  1167 \                                  isolate_bdvs False) e1_;            \

  1168 \       e2_ = Take (hd (tl es_));                                      \

  1169 \       e2_ = (Substitute [e1__]) e2_                                  \

  1170 \    in [e1_, e2_])";

  1171 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)

  1172 val str =

  1173 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \

  1174 \  (let e1_ = hd es_;                                                  \

  1175 \       v1_ = hd v_s;                                                  \

  1176 \       e2_ = Take (hd (tl es_));                                      \

  1177 \       e2_ = (Substitute [e1__]) e2_                                  \

  1178 \    in [e1_, e2_])";

  1179 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1180 (*---^^^-OK-----------------------------------------------------------------*)

  1181 (*---vvv-NOT ok-------------------------------------------------------------*)

  1182 val str =

  1183 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \

  1184 \  (let e1_ = hd es_;                                                  \

  1185 \       v1_ = hd v_s;                                                  \

  1186 \       xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \

  1187 \       e2_ = Take (hd (tl es_));                                      \

  1188 \       e2_ = (Substitute [e1__]) e2_                                  \

  1189 \    in [e1_, e2_])";

  1190 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)

  1191 val str = "if lhs e1_ =!= v1_ then 1 else 2";

  1192 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1194 val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";

  1195 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)

  1196 atomty sc; term2str sc;

  1198 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";

  1199 val str =

  1200 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

  1201 \  (let e2__ = Take (hd (tl es_));                                           \

  1202 \       e2__ = ((Substitute [e1__]) @@                                       \

  1203 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1204 \                                  simplify_System_parenthesized False)) @@  \

  1205 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1206 \                                  isolate_bdvs False))                  @@  \

  1207 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1208 \                                  simplify_System False)))             e2__;\

  1209 \       es__ = Take [e1__, e2__]                                             \

  1210 \   in (Try (Rewrite_Set order_system False)) es__)"

  1211 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1212 val str =

  1213 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

  1214 \  (let e2__ = Take (nth_ 2 es_);                                           \

  1215 \       e2__ = ((Substitute [e1__]) @@                                       \

  1216 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1217 \                                  simplify_System_parenthesized False)) @@  \

  1218 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1219 \                                  isolate_bdvs False))                  @@  \

  1220 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\

  1221 \                                  simplify_System False)))             e2__;\

  1222 \       es__ = Take [e1__, e2__]                                             \

  1223 \   in (Try (Rewrite_Set order_system False)) es__)"

  1224 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1225 val str =

  1226 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \

  1227 \  (let e2__ = Take (nth_ 2 es_);                                            \

  1228 \       e2__ = ((Substitute [e1__]) @@                                       \

  1229 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \

  1230 \                                  simplify_System_parenthesized False)) @@  \

  1231 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\

  1232 \                                  isolate_bdvs False))                  @@  \

  1233 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\

  1234 \                                  simplify_System False)))             e2__;\

  1235 \       es__ = Take [e1__, e2__]                                             \

  1236 \   in (Try (Rewrite_Set order_system False)) es__)"

  1237 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1238 val str =

  1239 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \

  1240 \  (let e2__ = Take (nth_ 2 es_);                                             \

  1241 \       e2__ = ((Substitute [e1__]) @@                                        \

  1242 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1243 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1244 \                                  simplify_System_parenthesized False)) @@   \

  1245 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \

  1246 \                                  isolate_bdvs False))                  @@   \

  1247 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \

  1248 \                                  norm_Rational False)))             e2__;   \

  1249 \       es__ = Take [e1__, e2__]                                              \

  1250 \   in [])"

  1251 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1252 val str =

  1253 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \

  1254 \  (let e2_ = Take (nth_ 2 es_);                                             \

  1255 \       e2_ = ((Substitute [e1_]) @@                                        \

  1256 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1257 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1258 \                                  simplify_System_parenthesized False)) @@   \

  1259 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \

  1260 \                                  isolate_bdvs False))                  @@   \

  1261 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \

  1262 \                                  norm_Rational False)))             e2_;   \

  1263 \       es_ = Take [e1_, e2_]                                              \

  1264 \   in [e1_, e2_,e3_, e4_])"

  1265 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1266 val str =

  1267 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \

  1268 \  (let e2_ = Take (nth_ 2 es_);                                              \

  1269 \       e2_ = ((Substitute [e1_]) @@                                          \

  1270 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1271 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1272 \                                  simplify_System_parenthesized False)) @@   \

  1273 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1274 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1275 \                                  isolate_bdvs False))                  @@   \

  1276 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1277 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1278 \                                  norm_Rational False)))             e2_;    \

  1279 \       es_ = Take [e1_, e2_]                                                 \

  1280 \   in [e1_, e2_,e3_, e4_])"

  1281 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1282 (*---^^^-OK-----------------------------------------------------------------*)

  1283 val str =

  1284 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \

  1285 \  (let e2_ = Take (nth_ 2 es_);                                              \

  1286 \       e2_ = ((Substitute [e1_]) @@                                          \

  1287 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1288 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1289 \                                  simplify_System_parenthesized False)) @@   \

  1290 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1291 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1292 \                                  isolate_bdvs False))                  @@   \

  1293 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\

  1294 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\

  1295 \                                  norm_Rational False)))             e2_     \

  1296 \   in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"

  1297 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

  1298 (*---vvv-NOT ok-------------------------------------------------------------*)

  1299 atomty sc; term2str sc;

  1302 "----- 7.70 with met top_down_: me";

  1303 val fmz = ["equalities                                         \

  1304 	    \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",

  1305 	    "solveForVars [c, c_2, c_3, c_4]", "solution L"];

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

  1307   ("Biegelinie",["linear", "system"],["no_met"]);

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

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

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

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

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

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

  1314 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()

  1315 	  | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";

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

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

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

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

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

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

  1322 if nxt = ("End_Proof'", End_Proof') andalso

  1323    f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

  1324 then () else error "eqsystem.sml: 7.70 with met top_down_: me";

  1327 "------- Bsp 7.71";

  1328 states:=[];

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

  1330 	     "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",

  1331 	     "FunktionsVariable x"],

  1332 	    ("Biegelinie", ["Biegelinien"],

  1333 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1334 moveActiveRoot 1;

  1335 (*

  1336 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1337 ##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal

  1338 c c_2          |c c_2	      |1'		      |1': c c_2 |

  1339           c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |

  1340 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

  1341       c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)

  1342 val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \

  1343 \ 0 = c_4 + 0 / (-1 * EI),                            \

  1344 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\

  1345 \ 0 = c_3 + 0 / (-1 * EI)]";

  1347 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1348 states:=[];

  1349 CalcTree [(["Traegerlaenge L",

  1350 	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",

  1351 	    "Biegelinie y",

  1352 	    "Randbedingungen [y 0 = 0, y L = 0]",

  1353 	    "FunktionsVariable x"],

  1354 	   ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],

  1355 	    ["Biegelinien", "AusMomentenlinie"]))];

  1356 moveActiveRoot 1;

  1357 (*

  1358 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1359 *)

  1361 "------- Bsp 7.72b";

  1362 states:=[];

  1363 CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",

  1364 	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",

  1365 	    "FunktionsVariable x"],

  1366 	   ("Biegelinie", ["Biegelinien"],

  1367 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

  1368 moveActiveRoot 1;

  1369 (*

  1370 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1371 ##7.72b##      |ord. |subst.singles         |ord.triang.

  1372   c_2          |     |			    |c_2

  1373 c c_2	       |     |1:c_2 -> 2':c	    |c_2 c

  1374           c_4  |     |			    |

  1375 c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)

  1376 val t = str2term"[0 = c_2,                                            \

  1377 \ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \

  1378 \ 0 = c_4 + 0 / (-1 * EI),                            \

  1379 \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";

  1381 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1382 states:=[];

  1383 CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)

  1384 	    "Biegelinie y",

  1385 	    "Randbedingungen [y L = 0, y' L = 0]",

  1386 	    "FunktionsVariable x"],

  1387 	   ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],

  1388 	    ["Biegelinien", "AusMomentenlinie"]))];

  1389 moveActiveRoot 1;

  1390 (*

  1391 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

  1392 *)

  1395 "----------- 4x4 systems from Biegelinie -------------------------";

  1396 "----------- 4x4 systems from Biegelinie -------------------------";

  1397 "----------- 4x4 systems from Biegelinie -------------------------";

  1398 (*STOPPED.WN08?? replace this test with 7.70 *)

  1399 "----- Bsp 7.27";

  1400 val fmz = ["equalities \

  1401 	   \[0 = c_4,                           \

  1402 	   \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                       \

  1403 	   \ 0 = c_2,                                           \

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

  1405 	   "solveForVars [c, c_2, c_3, c_4]", "solution L"];

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

  1407   ("Biegelinie",["normalize", "4x4", "linear", "system"],

  1408    ["EqSystem","normalize","4x4"]);

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

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

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

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

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

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

  1415 "------------------------------------------- Apply_Method...";

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

  1417 "[0 = c_4,                                          \

  1418 \ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                   \

  1419 \ 0 = c_2,                                          \

  1420 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";

  1421 (*vvvWN080102 Exception- Match raised

  1422   since assod Rewrite .. Rewrite'_Set

  1423 "------------------------------------------- simplify_System_parenthesized...";

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

  1425 "[0 = c_4,                                  \

  1426 \ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) +     \

  1427 \     (4 * L ^^^ 3 * c / (-24 * EI) +       \

  1428 \     (12 * L ^^^ 2 * c_2 / (-24 * EI) +    \

  1429 \     (L * c_3 + c_4))),                    \

  1430 \ 0 = c_2,                                  \

  1431 \ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";

  1432 (*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)

  1433 "------------------------------------------- isolate_bdvs...";

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

  1435 "[c_4 = 0,\

  1436 \ c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 4 / (-24 * EI)) + -1 * (4 * L ^^^ 3 * c / (-24 * EI)) + -1 * (12 * L ^^^ 2 * c_2 / (-24 * EI)) + -1 * (L * c_3),\

  1437 \ c_2 = 0, \

  1438 \ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";

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

  1441 ---------------------------------------------------------------------*)

  1443 (*

  1444 use"../smltest/IsacKnowledge/eqsystem.sml";

  1445 use"eqsystem.sml";

  1446 *)

  1447 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 06 May 2011 11:18:07 +0200
branch	decompose-isar
changeset 41977	a3ce4017f41d
parent 41943	f33f6959948b
child 42166	911c49949ba9
permissions	-rw-r--r--