1 (* "Knowledge/biegelinie-3.sml"
2 author: Walther Neuper 190515
3 (c) due to copyright terms
5 "table of contents -----------------------------------------------";
6 "-----------------------------------------------------------------";
7 "----------- see biegelinie-1.sml---------------------------------";
8 (* problems with generalised handling of meths which extend the model of a probl
9 since 98298342fb6d: wait for review of whole model-specify phase *)
10 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
11 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
12 "-----------------------------------------------------------------";
13 "-----------------------------------------------------------------";
14 "-----------------------------------------------------------------";
16 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
17 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
18 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
19 "----- Bsp 7.70 with me";
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"]);
26 val p = e_pos'; val c = [];
27 (*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
28 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
30 (*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
31 (*+*)writeln (oris2str oris); (*[
32 (1, ["1"], #Given,Traegerlaenge, ["L"]),
33 (2, ["1"], #Given,Streckenlast, ["q_0"]),
34 (3, ["1"], #Find,Biegelinie, ["y"]),
35 (4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
36 (5, ["1"], #undef,FunktionsVariable, ["x"]),
37 (6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
38 (7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
39 (*+*)itms2str_ @{context} probl = "[]";
40 (*+*)itms2str_ @{context} meth = "[]";
41 (*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
43 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
44 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
45 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
46 (*[], 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*)
47 (*[], 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]"*)
48 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
49 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
50 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
51 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
52 (*----------- 10 -----------*)
53 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
54 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
55 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
57 (*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
58 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
59 (*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
60 and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
61 formal arg. "b" type-matches with several...actual args. "["dy","y"]"
64 formals: ["l","q","v","b","s","vs","id_abl"]
65 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]"]*)
67 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
69 (*locatetac is here for testing by me; step would suffice in me*)
70 case locatetac tac (pt,p) of
71 ("ok", (_, _, ptp)) => ptp
74 (*+*)p''' = ([1], Pbl);
75 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
76 (*+*)(*MISSING after locatetac:*)
77 (*+*)writeln (oris2str oris); (*[
78 (1, ["1"], #Given,Streckenlast, ["q_0"]),
79 (2, ["1"], #Given,FunktionsVariable, ["x"]),
80 (3, ["1"], #Find,Funktionen, ["funs'''"])]
85 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
86 val (mI, m) = Solve.mk_tac'_ tac;
87 val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
88 (*if*) member op = Solve.specsteps mI = false; (*else*)
90 loc_solve_ (mI,m) ptp;
91 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
93 Solve.solve m (pt, pos);
94 "~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
96 val {srls, ...} = Specify.get_met mI;
97 val itms = case get_obj I pt p of
98 PblObj {meth=itms, ...} => itms
99 | _ => error "solve Apply_Method: uncovered case get_obj"
100 val thy' = get_obj g_domID pt p;
101 val thy = Celem.assoc_thy thy';
102 val (is, env, ctxt, sc) = case Lucin.init_pstate ctxt itms mI of
103 (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
104 | _ => error "solve Apply_Method: uncovered case init_pstate"
105 val ini = Lucin.init_form thy sc env;
107 val NONE = (*case*) ini (*of*);
108 val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
109 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
110 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
111 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
113 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
114 (*+*)(*MISSING after locate_input_tactic:*)
115 (*+*)writeln (oris2str oris); (*[
116 (1, ["1"], #Given,Streckenlast, ["q_0"]),
117 (2, ["1"], #Given,FunktionsVariable, ["x"]),
118 (3, ["1"], #Find,Funktionen, ["funs'''"])]
123 "~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p),
124 (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt)) =
125 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
126 val thy = Celem.assoc_thy thy';
127 (*if*) l = [] orelse (
128 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
129 (assy ((*thy',*)ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
131 "~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
132 (((*thy',*)ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
133 (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
135 "~~~~~ fun assy , args:"; val (((*thy',*)ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
136 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
137 val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
138 (*+*)writeln (term2str stac); (*SubProblem
139 (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
140 [''Biegelinien'', ''ausBelastung''])
141 [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
145 | _ => error ("assy: call by " ^ pos'2str (p,p_));
146 val Ass (m,v', ctxt) = (*case*) associate pt ctxt (m, stac) (*of*);
148 "~~~~~ fun associate , args:"; val (pt, _, (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
149 (stac as Const ("Program.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
150 dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
152 val dI = HOLogic.dest_string dI';
153 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
154 val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
155 val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
156 val ags = TermC.isalist2list ags';
157 (*if*) mI = ["no_met"] = false; (*else*)
158 (* val (pI, pors, mI) = *)
159 (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
160 handle ERROR "actual args do not match formal args"
161 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
162 "~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
164 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
165 val pbt' = filter_out is_copy_named pbt
166 val cy = filter is_copy_named pbt
167 val oris' = matc thy pbt' ags []
168 val cy' = map (cpy_nam pbt' oris') cy
169 val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
172 (*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
174 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
175 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
176 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
177 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
178 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
179 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
180 (*----------- 20 -----------*)
181 (*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
182 (*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
183 ERROR itms2args: 'Biegelinie' not in itms*)
185 (*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
186 [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
187 ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
188 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
189 (*+*)if oris2str oris =
190 (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
191 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
192 writeln (oris2str oris); (*[
193 (1, ["1"], #Given,Streckenlast, ["q_0"]),
194 (2, ["1"], #Given,FunktionsVariable, ["x"]),
195 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
196 (*+*)if itms2str_ @{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''']))]"
197 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
198 writeln (itms2str_ @{context} probl); (*[
199 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
200 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
201 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
202 (*+*)if itms2str_ @{context} meth = "[]"
203 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
204 writeln (itms2str_ @{context} meth); (*[]*)
206 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
208 (*locatetac is here for testing by me; step would suffice in me*)
209 case locatetac tac (pt,p) of
210 ("ok", (_, _, ptp)) => ptp
212 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
213 val (mI, m) = Solve.mk_tac'_ tac;
214 val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
215 (*if*) member op = Solve.specsteps mI = true; (*then*)
217 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
218 "~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
219 (* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
221 "~~~~~ fun specify , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
222 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
223 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
224 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
225 val {ppc, pre, prls,...} = Specify.get_met mID
226 val thy = Celem.assoc_thy dI
227 val dI'' = if dI = Rule.e_domID then dI' else dI
228 val pI'' = if pI = Celem.e_pblID then pI' else pI
230 (*+*)writeln (oris2str oris); (*[
231 (1, ["1"], #Given,Streckenlast, ["q_0"]),
232 (2, ["1"], #Given,FunktionsVariable, ["x"]),
233 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
234 (*+*)writeln (pats2str' ppc);
235 (*["(#Given, (Streckenlast, q__q))
236 ","(#Given, (FunktionsVariable, v_v))
237 ","(#Given, (Biegelinie, id_fun))
238 ","(#Given, (AbleitungBiegelinie, id_abl))
239 ","(#Find, (Funktionen, fun_s))"]*)
240 (*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
241 (*["(#Given, (Streckenlast, q_q))
242 ","(#Given, (FunktionsVariable, v_v))
243 ","(#Find, (Funktionen, funs'''))"]*)
244 val oris = Specify.add_field' thy ppc oris
245 val met = if met = [] then pbl else met
246 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
248 (*+*)writeln (itms2str_ @{context} itms); (*[
249 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
250 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
251 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
253 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
255 if mI' = ["Biegelinien", "ausBelastung"]
257 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
258 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
259 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
260 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
261 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
262 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
263 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
264 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
266 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
269 [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
270 [@{term "y::real \<Rightarrow> real"}]),
271 (@{term "id_fun::real \<Rightarrow> real"},
272 [@{term "y::real \<Rightarrow> real"}] ))),
273 (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
274 [@{term "dy::real \<Rightarrow> real"}]),
275 (@{term "id_abl::real \<Rightarrow> real"},
276 [@{term "dy::real \<Rightarrow> real"}] )))]
278 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
279 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
280 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
281 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
282 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
283 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
284 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
285 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
287 if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
288 (*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
290 val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
291 val (p,_,f,nxt,_,pt) = me nxt p c pt;
292 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*----------- 30 -----------*)
297 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
298 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 (*----------- 40 -----------*)
303 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
304 val (p,_,f,nxt,_,pt) = me nxt p c pt;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 (*----------- 50 -----------*)
309 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*----------- 60 -----------*)
315 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*----------- 70 -----------*)
321 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*----------- 80 -----------*)
327 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*----------- 90 -----------*)
333 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*---------- 100 -----------*)
339 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*---------- 110 -----------*)
345 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*---------- 120 -----------*)
351 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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 (*---------- 130 -----------*)
357 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
366 ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
370 {Find = [Incompl "solution []"], Given =
372 "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]",
373 Incompl "solveForVars [c]"],
374 Relate = [], Where = [], With = []}) => ()
375 | _ => error "Bsp.7.70 me changed 1")
376 | _ => error "Bsp.7.70 me changed 2"
377 else error "Bsp.7.70 me changed 3";
378 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
380 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
381 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
382 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
383 (* the error in this test might be independent from introduction of y, dy
384 as arguments in IntegrierenUndKonstanteBestimmen2,
385 rather due to so far untested use of "auto" *)
386 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
387 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
388 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
389 "AbleitungBiegelinie dy"];
390 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
391 ["IntegrierenUndKonstanteBestimmen2"]);
394 CalcTree [(fmz, (dI',pI',mI'))];
398 (*[], Met*)autoCalculate 1 CompleteCalcHead;
399 (*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)
400 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
401 (*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
402 (*[2], Res*)autoCalculate 1 CompleteSubpbl;
403 (*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
404 (*[3], Met*)autoCalculate 1 CompleteCalcHead;
405 (*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
406 (*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
407 (*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
408 (*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
409 (*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
410 (*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
411 (*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
412 (*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
413 (*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
414 (*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)
415 (*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
416 (*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
417 (*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
418 (*(**)autoCalculate 1 (Step 1);
419 *** generate1: not impl.for Empty_Tac_
420 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
422 val ((pt,_),_) = get_calc 1;
423 val ip = get_pos 1 1;
424 val (Form f, tac, asms) = pt_extract (pt, ip);
426 if ip = ([3, 8, 1], Res) andalso
427 term2str 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]"
430 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
431 | _ => error "ERROR biegel.7.70 changed 1"
432 else error "ERROR biegel.7.70 changed 2";
433 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)