1 (* Title: Knowledge/eqsystem-2.sml
2 author: Walther Neuper 050826,
3 (c) due to copyright terms
6 Rewrite.trace_on := false; (*true false*)
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 "----------- occur_exactly_in ------------------------------------";
11 "----------- problems --------------------------------------------";
12 "----------- rewrite-order ord_simplify_System -------------------";
13 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
14 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
15 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
16 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
17 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
18 "----------- refine [linear,system]-------------------------------";
19 "----------- refine [2x2,linear,system] search error--------------";
20 "----------- me [EqSystem,normalise,2x2] -------------------------";
21 (*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####
22 vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)
23 "----------- me [linear,system] ..normalise..top_down_sub..-------";
24 "----------- all systems from Biegelinie -------------------------";
25 "----------- 4x4 systems from Biegelinie -------------------------";
26 "-----------------------------------------------------------------";
27 "-----------------------------------------------------------------";
28 "-----------------------------------------------------------------";
30 val thy = @{theory "EqSystem"};
31 val ctxt = Proof_Context.init_global thy;
33 "----------- me [linear,system] ..normalise..top_down_sub..-------";
34 "----------- me [linear,system] ..normalise..top_down_sub..-------";
35 "----------- me [linear,system] ..normalise..top_down_sub..-------";
38 \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
39 \ - 1 * q_0 / 24 * 0 \<up> 4),\
40 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
41 \ - 1 * q_0 / 24 * L \<up> 4)]",
42 "solveForVars [c, c_2]", "solution LL"];
44 ("Biegelinie",["LINEAR", "system"], ["no_met"]);
45 val p = e_pos'; val c = [];
46 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
47 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
48 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
49 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
51 case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
52 | _ => error "eqsystem.sml [linear,system] specify b";
53 val (p,_,f,nxt,_,pt) = me nxt p c pt;
54 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
55 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
56 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
59 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
60 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
61 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
62 then () else error "eqsystem.sml me simpl. before SubProblem b";
64 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
65 | _ => error "eqsystem.sml me [linear,system] SubProblem b";
67 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
68 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
69 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
70 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
72 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
73 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 val PblObj {probl,...} = get_obj I pt [5];
77 (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
79 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
80 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
81 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
83 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
84 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
85 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
86 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
87 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
88 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
89 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
90 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
92 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
93 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
97 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
98 "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
99 "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
100 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
103 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
106 "----------- all systems from Biegelinie -------------------------";
107 "----------- all systems from Biegelinie -------------------------";
108 "----------- all systems from Biegelinie -------------------------";
109 val thy = @{theory Isac_Knowledge}
111 [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
112 (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
117 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
118 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
119 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
122 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
123 ##7.27## ordered substs
125 c c_2 c_3 c_4 c c_2 1->2: c
127 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
128 val t = TermC.str2term
130 "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
132 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
133 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
135 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
136 then () else error "Bsp 7.27";
138 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
139 val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
140 val NONE = rewrite_set_ thy false norm_Rational t;
142 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
143 if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
144 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
146 "--- isolate_bdvs_4x4";
148 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
150 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
152 val SOME (t,_) = rewrite_set_ thy false order_system t;
156 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
158 CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
159 ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
161 "Randbedingungen [y L = 0, y' L = 0]",
162 "FunktionsVariable x"],
163 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
164 ["Biegelinien", "AusMomentenlinie"]))];
167 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
173 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
174 "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
175 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
178 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
179 ##7.69## ordered subst 2x2
181 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
183 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*)
184 val t = TermC.str2term
185 ("[0 = c_4 + 0 / (- 1 * EI), " ^
186 "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
187 "0 = c_3 + 0 / (- 1 * EI), " ^
188 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
193 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
194 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
195 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
198 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
203 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
205 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
206 val t = TermC.str2term
208 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
211 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
212 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
213 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
215 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
216 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
218 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
219 if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
220 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
222 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
224 "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
225 " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
226 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
228 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
229 if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
230 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"*)
231 "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
232 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
234 val SOME (t, _) = rewrite_set_ thy false order_system t;
235 if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
236 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"*)
237 "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
238 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
240 "----- 7.70 with met normalise: ";
241 val fmz = ["equalities" ^
243 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
245 "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
246 val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
247 val p = e_pos'; val c = [];
249 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
250 in next but one test below the same type error.
251 /-------------------------------------------------------\
252 Type unification failed
253 Type error in application: incompatible operand type
255 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
256 Operand: [c_4] :: 'b list
257 \-------------------------------------------------------/
259 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
260 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
261 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
262 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
263 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
264 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
265 | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
266 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
268 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
269 (*-----------------------------------vvvWN080102 Exception- Match raised
270 since associate Rewrite .. Rewrite_Set
271 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
276 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
277 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
280 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
281 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
282 --------------------------------------------------------------------------*)
283 ============ inhibit exn WN120314 ==============================================*)
285 "----- 7.70 with met top_down_: me";
287 "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
288 "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
290 ("Biegelinie",["LINEAR", "system"],["no_met"]);
291 val p = e_pos'; val c = [];
292 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
293 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
294 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
295 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
296 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
297 case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
298 | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
299 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
302 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
303 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
305 if p = ([], Res) andalso
306 (* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
307 f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
308 then () else error "eqsystem.sml: 7.70 with met top_down_: me";
312 CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
313 "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
314 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
315 "AbleitungBiegelinie dy"],
316 ("Biegelinie", ["Biegelinien"],
317 ["IntegrierenUndKonstanteBestimmen2"] ))];
320 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
321 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
322 c c_2 |c c_2 |1' |1': c c_2 |
323 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
324 c c_2 c_3 c_4 | c_4 |3' | |
325 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
326 val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
327 \ 0 = c_4 + 0 / (- 1 * EI), \
328 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
329 \ 0 = c_3 + 0 / (- 1 * EI)]";
331 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
333 CalcTree [(["Traegerlaenge L",
334 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
336 "Randbedingungen [y 0 = (0::real), y L = 0]",
337 "FunktionsVariable x"],
338 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
339 ["Biegelinien", "AusMomentenlinie"]))];
342 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
347 CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
348 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
349 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
350 "AbleitungBiegelinie dy"],
351 ("Biegelinie", ["Biegelinien"],
352 ["IntegrierenUndKonstanteBestimmen2"] ))];
355 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
356 ##7.72b## |ord. |subst.singles |ord.triang.
358 c c_2 | |1:c_2 -> 2':c |c_2 c
360 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
361 val t = TermC.str2term"[0 = c_2, \
362 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
363 \ 0 = c_4 + 0 / (- 1 * EI), \
364 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
366 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
368 CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
370 "Randbedingungen [y L = 0, y' L = 0]",
371 "FunktionsVariable x"],
372 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
373 ["Biegelinien", "AusMomentenlinie"]))];
376 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
379 "----------- 4x4 systems from Biegelinie -------------------------";
380 "----------- 4x4 systems from Biegelinie -------------------------";
381 "----------- 4x4 systems from Biegelinie -------------------------";
382 (*STOPPED.WN08?? replace this test with 7.70 *)
384 val fmz = ["equalities \
386 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
388 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
389 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
391 ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
392 ["EqSystem", "normalise", "4x4"]);
393 val p = e_pos'; val c = [];
394 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
395 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
396 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
397 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
398 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
399 "------------------------------------------- Apply_Method...";
400 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
402 \ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
404 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
405 (*vvvWN080102 Exception- Match raised
406 since associate Rewrite .. Rewrite_Set
407 "------------------------------------------- simplify_System_parenthesized...";
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
410 \ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
411 \ (4 * L \<up> 3 * c / (- 24 * EI) + \
412 \ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
413 \ (L * c_3 + c_4))), \
415 \ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
416 (*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
417 "------------------------------------------- isolate_bdvs...";
418 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
420 \ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
422 \ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
423 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
425 ---------------------------------------------------------------------*)