1 (* Title: Knowledge/eqsystem-2.sml
2 author: Walther Neuper 050826,
3 (c) due to copyright terms
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "Knowledge/eqsystem-1.sml";
9 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
10 "----------- problems -----------------------------------------------------------equsystem-1.sml";
11 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
12 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
15 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
17 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
18 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
19 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
20 "Knowledge/eqsystem-1a.sml";
21 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
22 "Knowledge/eqsystem-2.sml";
23 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
24 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
25 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
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..-------";
36 val model = ["equalities " ^
37 "[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)," ^
38 " 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + - 1 * q_0 / 24 * L \<up> 4)]",
39 "solveForVars [c, c_2]", "solution LL"];
40 val refs = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
41 val p = e_pos'; val c = [];
42 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)];
43 val Model_Problem = nxt
44 val (p,_,f,nxt,_,pt) = me nxt p c pt;
45 val (p,_,f,nxt,_,pt) = me nxt p c pt;
46 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 Specify_Problem ["normalise", "2x2", "LINEAR", "system"] = nxt
49 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt
50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
51 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
52 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
53 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
54 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
55 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt
56 val "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]" = f2str f;
57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;
59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c, c_2]" = nxt
61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
62 val (p,_,f,nxt,_,pt) = me nxt p c pt;
63 val (p,_,f,nxt,_,pt) = me nxt p c pt;
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt
65 val (p,_,f,nxt,_,pt) = me nxt p c pt;
67 val PblObj {probl,...} = get_obj I pt [5];
69 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
70 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
71 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
72 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
73 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
78 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
79 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
80 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
81 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
83 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
84 "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
85 "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
86 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
89 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
92 "----------- all systems from Biegelinie -------------------------";
93 "----------- all systems from Biegelinie -------------------------";
94 "----------- all systems from Biegelinie -------------------------";
95 val thy = @{theory Isac_Knowledge}
97 [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"), (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),
98 (ParseC.parse_test @{context} "bdv_3", ParseC.parse_test @{context} "c_3"), (ParseC.parse_test @{context} "bdv_4", ParseC.parse_test @{context} "c_4")];
102 CalcTree @{context} [(
103 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
104 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
105 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
108 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
109 ##7.27## ordered substs
111 c c_2 c_3 c_4 c c_2 1->2: c
113 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
114 val t = ParseC.parse_test @{context}
116 "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), " ^
118 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
119 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;
120 if UnparseC.term @{context} t =
121 "[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]"
122 then () else error "Bsp 7.27";
124 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
125 val t = ParseC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
126 val NONE = rewrite_set_ ctxt false norm_Rational t;
128 rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
129 if UnparseC.term @{context} t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
130 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
132 "--- isolate_bdvs_4x4";
134 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
135 UnparseC.term @{context} t;
136 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;
137 UnparseC.term @{context} t;
138 val SOME (t,_) = rewrite_set_ ctxt false order_system t;
139 UnparseC.term @{context} t;
142 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
144 CalcTree @{context} [((*WN130908 <ERROR> error in kernel </ERROR>*)
145 ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
147 "Randbedingungen [y L = 0, y' L = 0]",
148 "FunktionsVariable x"],
149 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
150 ["Biegelinien", "AusMomentenlinie"]))];
153 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
158 CalcTree @{context} [(
159 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
160 "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
161 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
164 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
165 ##7.69## ordered subst 2x2
167 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
169 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*)
170 val t = ParseC.parse_test @{context}
171 ("[0 = c_4 + 0 / (- 1 * EI), " ^
172 "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), " ^
173 "0 = c_3 + 0 / (- 1 * EI), " ^
174 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
178 CalcTree @{context} [(
179 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
180 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
181 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
184 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
189 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
191 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
192 val t = ParseC.parse_test @{context}
194 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
197 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
198 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
199 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
200 if UnparseC.term @{context} t =
201 "[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]"
202 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
204 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
205 if UnparseC.term @{context} t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
206 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
208 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
209 if UnparseC.term @{context} t =
210 "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
211 " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
212 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
214 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
215 if UnparseC.term @{context} t =
216 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
217 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
219 val SOME (t, _) = rewrite_set_ ctxt false order_system t;
220 if UnparseC.term @{context} t =
221 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
222 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
224 "----- 7.70 with met normalise: ";
225 val fmz = ["equalities" ^
227 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
229 "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
230 val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
231 val p = e_pos'; val c = [];
233 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
234 in next but one test below the same type error.
235 /-------------------------------------------------------\
236 Type unification failed
237 Type error in application: incompatible operand type
239 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
240 Operand: [c_4] :: 'b list
241 \-------------------------------------------------------/
243 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
244 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
249 | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
252 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
253 (*-----------------------------------vvvWN080102 Exception- Match raised
254 since associate Rewrite .. Rewrite_Set
255 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
257 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
258 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
261 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
262 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
263 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
264 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
265 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
266 --------------------------------------------------------------------------*)
267 ============ inhibit exn WN120314 ==============================================*)
269 "----- 7.70 with met top_down_: me";
271 "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]",
272 "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
274 ("Biegelinie",["LINEAR", "system"],["no_met"]);
275 val p = e_pos'; val c = [];
276 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
277 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
280 val (p,_,f,nxt,_,pt) = me nxt p c pt;
281 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2, c, c_3, c_4]" = nxt
282 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["EqSystem", "top_down_substitution", "4x4"] = nxt
285 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
286 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
288 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
290 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
293 val "c = L * q_0" = f2str f;
294 (* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]" before NEW item_to_add*)
299 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
300 "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
301 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
302 "AbleitungBiegelinie dy"],
303 ("Biegelinie", ["Biegelinien"],
304 ["IntegrierenUndKonstanteBestimmen2"] ))];
307 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
308 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
309 c c_2 |c c_2 |1' |1': c c_2 |
310 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
311 c c_2 c_3 c_4 | c_4 |3' | |
312 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
313 val t = ParseC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
314 \ 0 = c_4 + 0 / (- 1 * EI), \
315 \ 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),\
316 \ 0 = c_3 + 0 / (- 1 * EI)]";
319 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
321 CalcTree @{context} [(["Traegerlaenge L",
322 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
324 "Randbedingungen [y 0 = (0::real), y L = 0]",
325 "FunktionsVariable x"],
326 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
327 ["Biegelinien", "AusMomentenlinie"]))];
330 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
335 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
336 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
337 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
338 "AbleitungBiegelinie dy"],
339 ("Biegelinie", ["Biegelinien"],
340 ["IntegrierenUndKonstanteBestimmen2"] ))];
343 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
344 ##7.72b## |ord. |subst.singles |ord.triang.
346 c c_2 | |1:c_2 -> 2':c |c_2 c
348 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
349 val t = ParseC.parse_test @{context}"[0 = c_2, \
350 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
351 \ 0 = c_4 + 0 / (- 1 * EI), \
352 \ 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)]";
354 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
356 CalcTree @{context} [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
358 "Randbedingungen [y L = 0, y' L = 0]",
359 "FunktionsVariable x"],
360 ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
361 ["Biegelinien", "AusMomentenlinie"]))];
364 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
368 "----------- 4x4 systems from Biegelinie -------------------------";
369 "----------- 4x4 systems from Biegelinie -------------------------";
370 "----------- 4x4 systems from Biegelinie -------------------------";
371 (*STOPPED.WN08?? replace this test with 7.70 *)
373 val fmz = ["equalities \
375 \ 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), \
377 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
378 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
380 ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
381 ["EqSystem", "normalise", "4x4"]);
382 val p = e_pos'; val c = [];
383 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [0 = c_4]" = nxt
385 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities\n [0 =\n c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_4, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" = nxt
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2, c, c_3, c_4]" = nxt
390 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
391 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
392 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["EqSystem", "normalise", "4x4"] = nxt
393 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
394 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt
395 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt
396 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt
397 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt
398 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "simplify_System_parenthesized") = nxt
399 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "isolate_bdvs_4x4") = nxt
400 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "simplify_System_parenthesized") = nxt
401 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "order_system" = nxt
402 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) = nxt
403 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
404 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, c_4 = 0]" = nxt
405 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, c_4 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt
406 (*WN231124 -------------------------------strange---^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^*)
407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities\n [c_4 = 0, c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2,\n L \<up> 3 * c / - 6 +\n (L \<up> 2 * c_2 / - 2 + (- 1 * L * c_3 / - 1 + - 1 * c_4 / - 1)) =\n q_0 * L \<up> 4 / - 24]" = nxt
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
410 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
411 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
412 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
413 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
414 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
415 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
416 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
418 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
419 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
420 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["EqSystem", "normalise", "4x4"] = nxt
421 val (p,_,f,nxt,_,pt) = me nxt p c pt;
422 val "[c_4 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0,\n - 1 * L \<up> 3 * c / 6 + (- 1 * L \<up> 2 * c_2 / 2 + (L * c_3 + c_4)) =\n q_0 * L \<up> 4 / - 24]"
424 (*WN231124 probably does not terminate*)
427 " 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)," ^
429 " 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";