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

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

     9 val thy = EqSystem.thy;

    11 "-----------------------------------------------------------------";

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

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

    14 "----------- occur_exactly_in ------------------------------------";

    15 "----------- problems --------------------------------------------";

    16 "----------- rewrite-order ord_simplify_System -------------------";

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

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

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

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

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

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

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

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

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

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

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

    28 "----------- all systems from Biegelinie -------------------------";

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

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

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

    32 "-----------------------------------------------------------------";

    35 "----------- occur_exactly_in ------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

    54 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 ()

    55 else raise error "eval_occur_exactly_in [c, c_2]";

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

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

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

    60 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 ()

    61 else raise error "eval_occur_exactly_in [c, c_2, c_3]";

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

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

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

    66 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 ()

    67 else raise error "eval_occur_exactly_in [c, c_2, c_3]";

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

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

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

    72 else raise error "eval_occur_exactly_in [c, c_2, c_3]";

    74 val t =

    75     str2term

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

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

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

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

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

    83 "----------- problems --------------------------------------------";

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

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

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

    87 atomty t;

    88 val testrls = append_rls "testrls" e_rls

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

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

    91 			  Calc ("op +", eval_binop "#add_"),

    92 			  Calc ("op =",eval_equal "#equal_")

    93 			  ];

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

    95 if term2str t' = "True" then ()

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

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

    99 atomty (term_of t);

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

   101 atomty (term_of t);

   103 val t = str2term

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

   105 atomty t;

   106 val t = str2term

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

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

   109 val SOME (t,_) =

   110     rewrite_set_ thy true

   111 		 (append_rls "prls_" e_rls

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

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

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

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

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

   117 				    eval_occur_exactly_in

   118 					"#eval_occur_exactly_in_")

   119 			      ]) t;

   120 if t = HOLogic.true_const then ()

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

   124 "----------- rewrite-order ord_simplify_System -------------------";

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

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

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

   128 "--- add_commute ---";

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

   130 				       str2term"c * x") then ()

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

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

   134 				       str2term"c_2") then ()

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

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

   138 				       str2term"c_2") then ()

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

   141 "--- mult_commute ---";

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

   143 				       str2term"c * x") then ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   183 val t =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   204 val xxx = rewrite_set_ thy true order_system t;

   205 if is_none xxx

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

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

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

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

   212 val e1__ = str2term "c_2 = 77";

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

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

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

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

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

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

   220 val SOME (e2__,_) =

   221     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;

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

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

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

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

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

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

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

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

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

   234 if not (ord_simplify_System

   235 	    false thy []

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

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

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

   240 trace_rewrite:=true;

   241 trace_rewrite:=false;

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

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

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

   247 (*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)

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

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

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

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

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

   253 	    (str2term"bdv_2",str2term"c_2"),

   254 	    (str2term"bdv_3",str2term"c_3"),

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

   256 val SOME (t,_) =

   257     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   286 val str =

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

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

   289 \                                simplify_System_parenthesized False) es_  \

   290 \   in ([]))";

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

   292 val str =

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

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

   295 \                                 simplify_System_parenthesized False) es_  \

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

   297 \                  []))";

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

   299 val str =

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

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

   302 \                                 simplify_System_parenthesized False) es_  \

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

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

   305 ;

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

   307 val str =

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

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

   310 \                                 simplify_System_parenthesized False) es_  \

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

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

   313 ;

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

   315 val str =

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

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

   318 \                                 simplify_System_parenthesized False)) es_  \

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

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

   321 ;

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

   323 val str =

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

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

   326 \                                 simplify_System_parenthesized False)) @@\

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

   328 \                                 simplify_System_parenthesized False))) es_\

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

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

   331 ;

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

   333 val str =

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

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

   336 \                                 simplify_System_parenthesized False)) @@\

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

   338 \                                 simplify_System_parenthesized False)) @@\

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

   340 \                                 simplify_System_parenthesized False))) es_\

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

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

   343 ;

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

   345 val str =

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

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

   348 \                                 simplify_System_parenthesized False)) @@\

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

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

   351 \                                 simplify_System_parenthesized False)) @@\

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

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

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

   355 ;

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

   357 val str =

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

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

   360 \                                 simplify_System_parenthesized False)) @@\

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

   362 \                                                    isolate_bdvs False)) @@\

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

   364 \                                 simplify_System_parenthesized False)) @@\

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

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

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

   368 ;

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

   370 val str =

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

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

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

   374 \                                                    isolate_bdvs False)) @@\

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

   376 \                                 simplify_System_parenthesized False)) @@\

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

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

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

   380 ;

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

   382 (*---^^^-OK-----------------------------------------------------------------*)

   383 (*---vvv-NOT ok-------------------------------------------------------------*)

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

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

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

   389 val str =

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

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

   392 \                                 simplify_System_parenthesized False) es_  \

   393 \   in ([]))";

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

   395 val str =

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

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

   398 \   in ([]))";

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

   400 val str =

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

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

   403 \       e1__ = Take (hd es_)                \

   404 \   in ([]))";

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

   406 val str =

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

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

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

   410 \   in ([]))";

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

   412 val str =

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

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

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

   416 \   in ([]))";

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

   418 (*--------------------------------------------------------------------------*)

   419 val str =

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

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

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

   423 (*--------------------------------------------------------------------------*)

   424 val str =

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

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

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

   428 \                                           isolate_bdvs False)) e1__\

   429 \   in ([]))";

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

   431 val str =

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

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

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

   435 \                                           isolate_bdvs False)) @@\

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

   437 \                                 simplify_System False)) e1__\

   438 \   in ([]))";

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

   440 val str =

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

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

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

   444 \                                           isolate_bdvs False)) @@\

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

   446 \                                 simplify_System False))) e1__\

   447 \   in ([]))";

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

   449 val str =

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

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

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

   453 \                                           isolate_bdvs False)) @@          \

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

   455 \                                 simplify_System False))) e1__;           \

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

   457 \   in ([]))";

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

   459 val str =

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

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

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

   463 \                                           isolate_bdvs False)) @@          \

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

   465 \                                 simplify_System False))) e1__;           \

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

   467 \       e2__ = Substitute [e1__] e2__                                       \

   468 \   in ([]))";

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

   470 val str =

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

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

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

   474 \                                           isolate_bdvs False)) @@          \

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

   476 \                                 simplify_System False))) e1__;           \

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

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

   479 \   in ([]))";

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

   481 val str =

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

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

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

   485 \                                      isolate_bdvs False)) @@               \

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

   487 \                                 simplify_System False))) e1__;           \

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

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

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

   491 \                                      isolate_bdvs False)) @@               \

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

   493 \                                 simplify_System False))) e2__            \

   494 \   in [e1__, e2__])"

   495 ;

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

   497 val str =

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

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

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

   501 \                                      isolate_bdvs False)) @@               \

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

   503 \                                 simplify_System False))) e1__;           \

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

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

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

   507 \                                 simplify_System_parenthesized False)) @@ \

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

   509 \                                      isolate_bdvs False)) @@               \

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

   511 \                                 simplify_System False)) @@               \

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

   513 \   in [e1__, e2__])"

   514 ;

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

   516 (*---^^^-OK-----------------------------------------------------------------*)

   517 val str =

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

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

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

   521 \                                      isolate_bdvs False)) @@               \

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

   523 \                                 simplify_System False))) e1__;           \

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

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

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

   527 \                                 simplify_System_parenthesized False)) @@ \

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

   529 \                                      isolate_bdvs False)) @@               \

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

   531 \                                 simplify_System False))) e2__;           \

   532 \       es__ = Take [e1__, e2__]\

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

   534 ;

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

   536 (*---vvv-NOT ok-------------------------------------------------------------*)

   537 atomty sc;

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

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

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

   542 val str =

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

   544 \  (let es__ = Take es_;   \

   545 \       e1__ = hd es__\

   546 \   in ([]))"

   547 ;

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

   549 val str =

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

   551 \  (let es__ = Take es_;   \

   552 \       e1__ = hd es__;    \

   553 \       e2__ = hd (tl es__)\

   554 \   in ([]))"

   555 ;

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

   557 val str =

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

   559 \  (let es__ = Take es_;   \

   560 \       e1__ = hd es__;    \

   561 \       e2__ = hd (tl es__);\

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

   563 \   in ([]))"

   564 ;

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

   566 val str =

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

   568 \  (let es__ = Take es_;   \

   569 \       e1__ = hd es__;    \

   570 \       e2__ = hd (tl es__);\

   571 \       es__ = [e1__,e2__]\

   572 \   in ([]))"

   573 ;

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

   575 val str =

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

   577 \  (let es__ = Take es_;   \

   578 \       e1__ = hd es__;    \

   579 \       e2__ = hd (tl es__);\

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

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

   582 \                                 simplify_System False)) es__            \

   583 \   in ([]))"

   584 ;

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

   586 val str =

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

   588 \  (let es__ = Take es_;   \

   589 \       e1__ = hd es__;    \

   590 \       e2__ = hd (tl es__);\

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

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

   593 \                                      isolate_bdvs False)) @@               \

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

   595 \                                 simplify_System False))) es__            \

   596 \   in ([]))"

   597 ;

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

   599 val str =

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

   601 \  (let es__ = Take es_;   \

   602 \       e1__ = hd es__;    \

   603 \       e2__ = hd (tl es__);\

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

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

   606 \                                 simplify_System_parenthesized False)) @@  \

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

   608 \                                      isolate_bdvs False)) @@               \

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

   610 \                                 simplify_System False))) es__            \

   611 \   in ([]))"

   612 ;

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

   614 val str =

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

   616 \  (let es__ = Take es_;                                                     \

   617 \       e1__ = hd es__;                                                      \

   618 \       e2__ = hd (tl es__);                                                 \

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

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

   621 \                                 simplify_System_parenthesized False)) @@  \

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

   623 \                                      isolate_bdvs False))              @@  \

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

   625 \                                 simplify_System False))) es__            \

   626 \   in es__)"

   627 ;

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

   629 val str =

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

   631 \  (let es__ = Take es_;                                              \

   632 \       e1__ = hd es__;                                               \

   633 \       e2__ = hd (tl es__);                                          \

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

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

   636 \                                 simplify_System_parenthesized False)) @@   \

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

   638 \                              isolate_bdvs False))              @@   \

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

   640 \                                 simplify_System False))) es__)"

   641 ;

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

   643 (*---^^^-OK-----------------------------------------------------------------*)

   644 val str =

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

   646 \  (let es__ = Take es_;                                              \

   647 \       e1__ = hd es__;                                               \

   648 \       e2__ = hd (tl es__);                                          \

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

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

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

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

   653 \                                 simplify_System_parenthesized False)) @@   \

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

   655 \                              isolate_bdvs False))              @@   \

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

   657 \                                 simplify_System False))) es__)"

   658 ;

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

   660 (*---vvv-NOT ok-------------------------------------------------------------*)

   661 atomty sc;

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

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

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

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

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

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

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

   671 case matches of [_,_,_,

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

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

   674 			   With = [],

   675 			   Given =

   676 			   [Correct

   677 				"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]",

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

   679 			   Where = [],

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

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

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

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

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

   687 case matches of [_,_,

   688 		 Matches

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

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

   691 		       With = [],

   692 		       Given =

   693 		       [Correct

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

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

   696 		       Where =

   697 		       [Correct

   698 			    "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]",

   699 			    Correct

   700 				"[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]"],

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

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

   705 (*WN051014----------------------------------------------------------------

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

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

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

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

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

   711 (*... resulted in

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

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

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

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

   717 trace_rewrite:=true;

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

   719 (*found:...

   720 ##  try thm: nth_Cons_

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

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

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

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

   725 #####  try calc: op <'

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

   728 ... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)

   729 trace_rewrite:=false;

   730 (*WN051014------------------------------------------------------------------*)

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

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

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

   735 	   \            0 = c_4,                           \

   736 	   \            0 = c_3]",

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

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

   739 (* trace_rewrite := true;

   740    trace_rewrite := false;

   741    *)

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

   743 case matches of

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

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

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

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

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

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

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

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

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

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

   755 	   \            0 = c_3,                           \

   756 	   \            0 = c_4]",

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

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

   759 (* print_depth 11; matches; print_depth 3;

   760    *)

   761 case matches of

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

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

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

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

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

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

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

   771   we investigated in these steps:*)

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

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

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

   775 trace_rewrite:=true;

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

   777 trace_rewrite:=false;

   778 print_depth 11; matches; print_depth 3;

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

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

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

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

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

   785    *)

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

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

   789 =========================================================================\

   790 -------fun prep_pbt

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

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

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

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

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

   796 			],

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

   798 		       SOME "solveSystem es_ v_s",

   799 		       []));

   800    *)

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

   802 val equalities_es_ = "equalities es_" : string

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

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

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

   806 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

   811 =========================================================================/

   815 -----fun refin' ff:

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

   817 [

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

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

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

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

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

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

   825 > (writeln o pres2str) pre';

   826 [

   827 (false, length_ es_ = 2),

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

   830 ----- fun match_oris':

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

   832 > (writeln o pres2str) pre';

   833 ..as in refin'

   835 ----- fun check_preconds'

   836 > (writeln o env2str) env;

   837 ["

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

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

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

   841 (ss___, L)"]

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

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

   846 > val pre1 = hd pres;

   847 atomty pre1;

   848 ***

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

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

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

   852 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~

   853 *** . Free (2, real)

   854 ***

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

   857 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   858 *)

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

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

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   900 (*[

   901 (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]])),

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

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

   904 *)

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

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

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

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

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

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

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

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

   920 case nxt of

   921     (_, End_Proof') => ()

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

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

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

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

   928 val fmz =

   929     ["equalities\

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

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

   954 case nxt of

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

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

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

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

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

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

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

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

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

   969 (*[

   970 (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]])),

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

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

   973 *)

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

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

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

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

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

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

   987 if f2str f =

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

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

   990 case nxt of

   991     (_, End_Proof') => ()

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

   995 "----------- all systems from Biegelinie -------------------------";

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

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

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

   999 	     (str2term "bdv_2", str2term "c_2"),

  1000 	     (str2term "bdv_3", str2term "c_3"),

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

  1002 "------- Bsp 7.27";

  1003 states:=[];

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

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

  1006 	     "FunktionsVariable x"],

  1007 	    ("Biegelinie", ["Biegelinien"],

  1008 		     ["IntegrierenUndKonstanteBestimmen2"]))];

  1009 moveActiveRoot 1;

  1010 (*

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

  1012 ##7.27##          ordered           substs

  1013           c_4       c_2

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

  1015   c_2                       c_4

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

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

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

  1019 \ 0 = c_2,                                           \

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

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

  1022 term2str t';

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

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

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

  1028 val NONE = rewrite_set_ thy false norm_Rational t;

  1029 val SOME (t,_) =

  1030     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

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

  1032 "--- isolate_bdvs_4x4";

  1033 (*

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

  1035 term2str t;

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

  1037 term2str t;

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

  1039 term2str t;

  1040 *)

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

  1043 states:=[];

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

  1045 	    "Biegelinie y",

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

  1047 	    "FunktionsVariable x"],

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

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

  1050 moveActiveRoot 1;

  1051 (*

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

  1053 *)

  1055 "------- Bsp 7.69";

  1056 states:=[];

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

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

  1059 	     "FunktionsVariable x"],

  1060 	    ("Biegelinie", ["Biegelinien"],

  1061 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1062 moveActiveRoot 1;

  1063 (*

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

  1065 ##7.69##          ordered           subst                   2x2

  1066           c_4           c_3

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

  1068       c_3                   c_4

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

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

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

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

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

  1075 "------- Bsp 7.70";

  1076 states:=[];

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

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

  1079 	     "FunktionsVariable x"],

  1080 	    ("Biegelinie", ["Biegelinien"],

  1081 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1082 moveActiveRoot 1;

  1083 (*

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

  1085 ##7.70##        |subst

  1086 c		|

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

  1088       c_3	|

  1089           c_4   |            GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)

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

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

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

  1094 		\ 0 = c_4,                           \

  1095 		\ 0 = c_3]";

  1096 val SOME (t,_) =

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

  1098 val SOME (t,_) =

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

  1100 val SOME (t,_) =

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

  1102 term2str t =

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

  1104 val SOME (t,_) =

  1105     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

  1106 term2str t =

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

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

  1109 term2str t =

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

  1111 val SOME (t,_) =

  1112     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

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

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

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

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

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

  1121 val fmz = ["equalities                                         \

  1122 	    \[L * q_0 = c,                       \

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

  1124 		\ 0 = c_4,                           \

  1125 		\ 0 = c_3]",

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

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

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

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

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

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

  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 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()

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

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

  1138 "bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";

  1139 (*vvvWN080102 Exception- Match raised

  1140   since assod Rewrite .. Rewrite'_Set

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

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

  1146 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 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"

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

  1152 --------------------------------------------------------------------------*)

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

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

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

  1157 val str =

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

  1159 \  (let e1_ = hd es_;                                                  \

  1160 \       v1_ = hd v_s;                                                  \

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

  1162 \             then 0=0                                                 \

  1163 \             else let e1_ = Take e1_;                                 \

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

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

  1166 \                                  isolate_bdvs False) e1_;            \

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

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

  1169 \    in [e1_, e2_])";

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

  1171 val str =

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

  1173 \  (let e1_ = hd es_;                                                  \

  1174 \       v1_ = hd v_s;                                                  \

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

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

  1177 \    in [e1_, e2_])";

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

  1179 (*---^^^-OK-----------------------------------------------------------------*)

  1180 (*---vvv-NOT ok-------------------------------------------------------------*)

  1181 val str =

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

  1183 \  (let e1_ = hd es_;                                                  \

  1184 \       v1_ = hd v_s;                                                  \

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

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

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

  1188 \    in [e1_, e2_])";

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

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

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

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

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

  1195 atomty sc; term2str sc;

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

  1198 val str =

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

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

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

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

  1203 \                                  simplify_System_parenthesized False)) @@  \

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

  1205 \                                  isolate_bdvs False))                  @@  \

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

  1207 \                                  simplify_System False)))             e2__;\

  1208 \       es__ = Take [e1__, e2__]                                             \

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

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

  1211 val str =

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

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

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

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

  1216 \                                  simplify_System_parenthesized False)) @@  \

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

  1218 \                                  isolate_bdvs False))                  @@  \

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

  1220 \                                  simplify_System False)))             e2__;\

  1221 \       es__ = Take [e1__, e2__]                                             \

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

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

  1224 val str =

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

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

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

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

  1229 \                                  simplify_System_parenthesized False)) @@  \

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

  1231 \                                  isolate_bdvs False))                  @@  \

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

  1233 \                                  simplify_System False)))             e2__;\

  1234 \       es__ = Take [e1__, e2__]                                             \

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

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

  1237 val str =

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

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

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

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

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

  1243 \                                  simplify_System_parenthesized False)) @@   \

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

  1245 \                                  isolate_bdvs False))                  @@   \

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

  1247 \                                  norm_Rational False)))             e2__;   \

  1248 \       es__ = Take [e1__, e2__]                                              \

  1249 \   in [])"

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

  1251 val str =

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

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

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

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

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

  1257 \                                  simplify_System_parenthesized False)) @@   \

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

  1259 \                                  isolate_bdvs False))                  @@   \

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

  1261 \                                  norm_Rational False)))             e2_;   \

  1262 \       es_ = Take [e1_, e2_]                                              \

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

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

  1265 val str =

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

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

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

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

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

  1271 \                                  simplify_System_parenthesized False)) @@   \

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

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

  1274 \                                  isolate_bdvs False))                  @@   \

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

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

  1277 \                                  norm_Rational False)))             e2_;    \

  1278 \       es_ = Take [e1_, e2_]                                                 \

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

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

  1281 (*---^^^-OK-----------------------------------------------------------------*)

  1282 val str =

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

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

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

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

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

  1288 \                                  simplify_System_parenthesized False)) @@   \

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

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

  1291 \                                  isolate_bdvs False))                  @@   \

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

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

  1294 \                                  norm_Rational False)))             e2_     \

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

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

  1297 (*---vvv-NOT ok-------------------------------------------------------------*)

  1298 atomty sc; term2str sc;

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

  1302 val fmz = ["equalities                                         \

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

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

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

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

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

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

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

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

  1314 	  | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";

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

  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 if nxt = ("End_Proof'", End_Proof') andalso

  1322    f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

  1323 then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";

  1326 "------- Bsp 7.71";

  1327 states:=[];

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

  1329 	     "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",

  1330 	     "FunktionsVariable x"],

  1331 	    ("Biegelinie", ["Biegelinien"],

  1332 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

  1333 moveActiveRoot 1;

  1334 (*

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

  1336 ##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal

  1337 c c_2          |c c_2	      |1'		      |1': c c_2 |

  1338           c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |

  1339 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

  1340       c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)

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

  1342 \ 0 = c_4 + 0 / (-1 * EI),                            \

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

  1344 \ 0 = c_3 + 0 / (-1 * EI)]";

  1346 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1347 states:=[];

  1348 CalcTree [(["Traegerlaenge L",

  1349 	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",

  1350 	    "Biegelinie y",

  1351 	    "Randbedingungen [y 0 = 0, y L = 0]",

  1352 	    "FunktionsVariable x"],

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

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

  1355 moveActiveRoot 1;

  1356 (*

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

  1358 *)

  1360 "------- Bsp 7.72b";

  1361 states:=[];

  1362 CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",

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

  1364 	    "FunktionsVariable x"],

  1365 	   ("Biegelinie", ["Biegelinien"],

  1366 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

  1367 moveActiveRoot 1;

  1368 (*

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

  1370 ##7.72b##      |ord. |subst.singles         |ord.triang.

  1371   c_2          |     |			    |c_2

  1372 c c_2	       |     |1:c_2 -> 2':c	    |c_2 c

  1373           c_4  |     |			    |

  1374 c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)

  1375 val t = str2term"[0 = c_2,                                            \

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

  1377 \ 0 = c_4 + 0 / (-1 * EI),                            \

  1378 \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";

  1380 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

  1381 states:=[];

  1382 CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)

  1383 	    "Biegelinie y",

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

  1385 	    "FunktionsVariable x"],

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

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

  1388 moveActiveRoot 1;

  1389 (*

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

  1391 *)

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

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

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

  1397 (*GOON replace this test with 7.70 *)

  1398 "----- Bsp 7.27";

  1399 val fmz = ["equalities \

  1400 	   \[0 = c_4,                           \

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

  1402 	   \ 0 = c_2,                                           \

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

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

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

  1406   ("Biegelinie",["normalize", "4x4", "linear", "system"],

  1407    ["EqSystem","normalize","4x4"]);

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

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

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

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

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

  1416 "[0 = c_4,                                          \

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

  1418 \ 0 = c_2,                                          \

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

  1420 (*vvvWN080102 Exception- Match raised

  1421   since assod Rewrite .. Rewrite'_Set

  1422 "------------------------------------------- simplify_System_parenthesized...";

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

  1424 "[0 = c_4,                                  \

  1425 \ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) +     \

  1426 \     (4 * L ^^^ 3 * c / (-24 * EI) +       \

  1427 \     (12 * L ^^^ 2 * c_2 / (-24 * EI) +    \

  1428 \     (L * c_3 + c_4))),                    \

  1429 \ 0 = c_2,                                  \

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

  1431 (*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)

  1432 "------------------------------------------- isolate_bdvs...";

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

  1434 "[c_4 = 0,\

  1435 \ 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),\

  1436 \ c_2 = 0, \

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

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

  1440 ---------------------------------------------------------------------*)

  1442 (*

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

  1444 use"eqsystem.sml";

  1445 *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 08 Sep 2010 17:49:36 +0200
branch	isac-update-Isa09-2
changeset 37995	fac82f29f143
parent 37991	028442673981
child 38014	3e11e3c2dc42
permissions	-rw-r--r--