1 (* "Knowledge/biegelinie-4.sml"
2 author: Walther Neuper 190515
3 (c) due to copyright terms
5 "table of contents ---------------------------------------------------------------------------";
6 "---------------------------------------------------------------------------------------------";
7 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
8 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me ---------------------------------";
9 "---------------------------------------------------------------------------------------------";
10 "---------------------------------------------------------------------------------------------";
11 "---------------------------------------------------------------------------------------------";
14 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
15 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
16 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
17 (* the error in this test might be independent from introduction of y, dy
18 as arguments in IntegrierenUndKonstanteBestimmen2,
19 rather due to so far untested use of "auto" *)
20 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
21 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
22 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
23 "AbleitungBiegelinie dy"];
24 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
25 ["IntegrierenUndKonstanteBestimmen2"]);
28 CalcTree [(fmz, (dI',pI',mI'))];
31 autoCalculate 1 CompleteCalc;
33 val ((pt, p),_) = get_calc 1;
34 if p = ([], Pbl) then () else error ""
35 get_obj I pt (fst p); (*TODO investigate failure*)
37 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ * )
38 (*[], Met*)autoCalculate 1 CompleteCalcHead;
39 (*[1], Pbl*)autoCalculate 1 (Steps 1); (* into SubProblem *)
40 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
41 (*[2], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)
42 (*[2], Res*)autoCalculate 1 CompleteSubpbl;
43 (*[3], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)
44 (*[3], Met*)autoCalculate 1 CompleteCalcHead;
45 (*[3, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
46 (*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: Step.add: not impl.for Empty_Tac_*)
47 (*[3, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
48 (*[3, 2], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
49 (*[3, 3], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
50 (*[3, 4], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
51 (*[3, 5], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
52 (*[3, 6], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
53 (*[3, 7], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
54 (*[3, 8], Pbl*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
55 (*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
56 (*[3, 8, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
57 (*[3, 8, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
58 (*(**)autoCalculate 1 (Steps 1);
59 *** Step.add: not impl.for Empty_Tac_
60 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
62 val ((pt,_),_) = get_calc 1;
64 val (Form f, tac, asms) = pt_extract (pt, ip);
66 if ip = ([3, 8, 1], Res) andalso
67 UnparseC.term f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"
70 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
71 | _ => error "ERROR biegel.7.70 changed 1"
72 else error "ERROR biegel.7.70 changed 2";
73 ( * NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
76 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
77 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
78 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
79 "----- Bsp 7.70 with me";
80 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
81 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
82 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
83 "AbleitungBiegelinie dy"];
84 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
85 ["IntegrierenUndKonstanteBestimmen2"]);
86 val p = e_pos'; val c = [];
87 (*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
88 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
90 (*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
91 (*+*)writeln (O_Model.to_string oris); (*[
92 (1, ["1"], #Given,Traegerlaenge, ["L"]),
93 (2, ["1"], #Given,Streckenlast, ["q_0"]),
94 (3, ["1"], #Find,Biegelinie, ["y"]),
95 (4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
96 (5, ["1"], #undef,FunktionsVariable, ["x"]),
97 (6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
98 (7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
99 (*+*)I_Model.to_string @{context} probl = "[]";
100 (*+*)I_Model.to_string @{context} meth = "[]";
101 (*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
103 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
104 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
105 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
106 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
107 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
108 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
109 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
110 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
111 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
112 (*----------- 10 -----------*)
113 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
114 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
115 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
117 (*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
118 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
119 (*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
120 and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
121 formal arg. "b" type-matches with several...actual args. "["dy","y"]"
124 formals: ["l","q","v","b","s","vs","id_abl"]
125 actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
127 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
129 (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
130 case Step.by_tactic tac (pt,p) of
131 ("ok", (_, _, ptp)) => ptp
134 (*+*)p''' = ([1], Pbl);
135 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
136 (*+*)(*MISSING after Step.by_tactic:*)
137 (*+*)writeln (O_Model.to_string oris); (*[
138 (1, ["1"], #Given,Streckenlast, ["q_0"]),
139 (2, ["1"], #Given,FunktionsVariable, ["x"]),
140 (3, ["1"], #Find,Funktionen, ["funs'''"])]
145 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
146 val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
147 (*if*) Library.member op = Solve.specsteps mI = false; (*else*)
149 loc_solve_ (mI,m) ptp;
150 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
152 Step_Solve.by_tactic m (pt, pos);
153 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
155 val {srls, ...} = Specify.get_met mI;
156 val itms = case get_obj I pt p of
157 PblObj {meth=itms, ...} => itms
158 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
159 val thy' = get_obj g_domID pt p;
160 val thy = ThyC.get_theory thy';
161 val srls = LItool.get_simplifier (pt, pos)
162 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
163 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
164 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
165 val ini = LItool.implicit_take sc env;
167 val NONE = (*case*) ini (*of*);
168 val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt;
169 val d = Rule_Set.empty (*FIXME: get simplifier from domID*);
170 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
171 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
173 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
174 (*+*)(*MISSING after locate_input_tactic:*)
175 (*+*)writeln (O_Model.to_string oris); (*[
176 (1, ["1"], #Given,Streckenlast, ["q_0"]),
177 (2, ["1"], #Given,FunktionsVariable, ["x"]),
178 (3, ["1"], #Find,Funktionen, ["funs'''"])]
183 "~~~~~ fun locate_input_tactic , args:"; val () = ();
186 (*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
188 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
189 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
190 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
191 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
192 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
193 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
194 (*----------- 20 -----------*)
195 (*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
196 (*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
197 ERROR arguments_from_model: 'Biegelinie' not in itms*)
199 (*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
200 [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
201 ^^^^^^^^^^^ ..ERROR arguments_from_model: 'Biegelinie' not in itms*)
202 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
203 (*+*)if O_Model.to_string oris =
204 (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
205 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
206 writeln (O_Model.to_string oris); (*[
207 (1, ["1"], #Given,Streckenlast, ["q_0"]),
208 (2, ["1"], #Given,FunktionsVariable, ["x"]),
209 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
210 (*+*)if I_Model.to_string @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"
211 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
212 writeln (I_Model.to_string @{context} probl); (*[
213 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
214 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
215 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
216 (*+*)if I_Model.to_string @{context} meth = "[]"
217 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
218 writeln (I_Model.to_string @{context} meth); (*[]*)
220 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
222 (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
223 case Step.by_tactic tac (pt,p) of
224 ("ok", (_, _, ptp)) => ptp
226 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
227 val Applicable.Yes m = (*case*) Step.check m (pt, p)(*of*);
228 (*if*) Library.member op = Solve.specsteps mI = true; (*then*)
230 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
231 "~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
232 (* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
234 "~~~~~ fun specify , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
235 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
236 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
237 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
238 val {ppc, pre, prls,...} = Specify.get_met mID
239 val thy = ThyC.get_theory dI
240 val dI'' = if dI = ThyC.id_empty then dI' else dI
241 val pI'' = if pI = Problem.id_empty then pI' else pI
243 (*+*)writeln (O_Model.to_string oris); (*[
244 (1, ["1"], #Given,Streckenlast, ["q_0"]),
245 (2, ["1"], #Given,FunktionsVariable, ["x"]),
246 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
247 (*+*)writeln (pats2str' ppc);
248 (*["(#Given, (Streckenlast, q__q))
249 ","(#Given, (FunktionsVariable, v_v))
250 ","(#Given, (Biegelinie, id_fun))
251 ","(#Given, (AbleitungBiegelinie, id_abl))
252 ","(#Find, (Funktionen, fun_s))"]*)
253 (*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
254 (*["(#Given, (Streckenlast, q_q))
255 ","(#Given, (FunktionsVariable, v_v))
256 ","(#Find, (Funktionen, funs'''))"]*)
257 val oris = Specify.add_field' thy ppc oris
258 val met = if met = [] then pbl else met
259 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
261 (*+*)writeln (I_Model.to_string @{context} itms); (*[
262 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
263 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
264 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
266 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
268 if mI' = ["Biegelinien", "ausBelastung"]
270 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
271 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
272 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
273 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
274 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
275 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
276 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
277 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
279 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
282 [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
283 [@{term "y::real \<Rightarrow> real"}]),
284 (@{term "id_fun::real \<Rightarrow> real"},
285 [@{term "y::real \<Rightarrow> real"}] ))),
286 (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
287 [@{term "dy::real \<Rightarrow> real"}]),
288 (@{term "id_abl::real \<Rightarrow> real"},
289 [@{term "dy::real \<Rightarrow> real"}] )))]
291 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
292 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
293 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
294 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
295 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
296 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
297 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
298 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
300 if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
301 (*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
303 val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
304 val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
306 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
309 (*----------- 30 -----------*)
310 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
311 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
312 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
313 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
314 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
315 (*----------- 40 -----------*)
316 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
317 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
318 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
319 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
320 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
321 (*----------- 50 -----------*)
322 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
323 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
324 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
325 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
326 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
327 (*----------- 60 -----------*)
328 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
329 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
330 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
332 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
333 (*----------- 70 -----------*)
334 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
335 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
336 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
337 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
338 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
339 (*----------- 80 -----------*)
340 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
341 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
342 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
343 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
344 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 (*----------- 90 -----------*)
346 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
347 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
348 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
349 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
350 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
351 (*---------- 100 -----------*)
352 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
353 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
354 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
355 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
356 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
357 (*---------- 110 -----------*)
358 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
359 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
360 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
361 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 (*---------- 120 -----------*)
364 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
365 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
366 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
367 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 (*---------- 130 -----------*)
370 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
372 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
373 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
374 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
383 {Find = [Incompl "solution []"], Given =
385 "equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
386 Incompl "solveForVars [c]"],
387 Relate = [], Where = [], With = []}) => ()
388 | _ => error "Bsp.7.70 me changed 1")
389 | _ => error "Bsp.7.70 me changed 2"
390 else error "Bsp.7.70 me changed 3";
391 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)