1 (* Title: "Specify/specify.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";
11 "----------- maximum-example: I_Model.complete -------------------------------------------------";
12 "----------- specify-phase: low level functions ------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
17 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";
18 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";
19 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";
20 (*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
21 val (p,_,f,nxt,_,pt) =
23 [(["fixedValues [r=Arbfix]", "maximum A",
25 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
26 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
27 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
29 "boundVariable a", "boundVariable b", "boundVariable alpha",
30 "interval {x::real. 0 <= x & x <= 2*r}",
31 "interval {x::real. 0 <= x & x <= 2*r}",
32 "interval {x::real. 0 <= x & x <= pi}",
33 "errorBound (eps=(0::real))"],
34 ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])
36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
38 val (p,_,f,nxt,_,pt) = me nxt p c pt;
39 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
40 val pits = get_obj g_pbl pt (fst p);
41 writeln (I_Model.to_string ctxt pits);
43 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
44 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
45 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
46 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
47 val (pt,p) = Specify.finish_phase (pt,p);
48 val pits = get_obj g_pbl pt (fst p);
49 if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
50 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
51 writeln (I_Model.to_string ctxt pits);
53 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
54 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
55 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
56 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
57 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
58 val mits = get_obj g_met pt (fst p);
59 if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
60 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
61 writeln (I_Model.to_string ctxt mits);
63 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
64 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
65 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
66 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
67 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
68 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
69 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
70 0 <= x & x <= 2 * r}])),
71 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
72 ( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
74 "----------- maximum-example: I_Model.complete -------------------------------------------------";
75 "----------- maximum-example: I_Model.complete -------------------------------------------------";
76 "----------- maximum-example: I_Model.complete -------------------------------------------------";
78 val (p,_,f,nxt,_,pt) =
80 [(["fixedValues [r=Arbfix]", "maximum A",
82 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
83 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
84 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
86 "boundVariable a", "boundVariable b", "boundVariable alpha",
87 "interval {x::real. 0 <= x & x <= 2*r}",
88 "interval {x::real. 0 <= x & x <= 2*r}",
89 "interval {x::real. 0 <= x & x <= pi}",
90 "errorBound (eps=(0::real))"],
91 ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e;*)
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 val (p,_,f,nxt,_,pt) = me nxt p c pt;
100 (*nxt = Specify_Theory "DiffApp"*)
101 val (oris, _, _) = get_obj g_origin pt (fst p);
102 writeln (O_Model.to_string oris);
104 (1, ["1", "2", "3"], #Given,fixedValues, ["[r = Arbfix]"]),
105 (2, ["1", "2", "3"], #Find,maximum, ["A"]),
106 (3, ["1", "2", "3"], #Find,valuesFor, ["[a]", "[b]"]),
107 (4, ["1", "2"], #Relate,relations, ["[A = a * b]", "[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
108 (5, ["3"], #Relate,relations, ["[A = a * b]", "[a / 2 = r * sin alpha]", "[b / 2 = r * cos alpha]"]),
109 (6, ["1"], #undef,boundVariable, ["a"]),
110 (7, ["2"], #undef,boundVariable, ["b"]),
111 (8, ["3"], #undef,boundVariable, ["alpha"]),
112 (9, ["1", "2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
113 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
114 (11, ["1", "2", "3"], #undef,errorBound, ["eps = 0"])]*)
115 val pits = get_obj g_pbl pt (fst p);
116 writeln (I_Model.to_string ctxt pits);
118 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
119 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
120 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
121 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
122 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
123 val mits = get_obj g_met pt (fst p);
124 val mits = I_Model.complete oris pits []
125 ((#ppc o Method.from_store) ["DiffApp", "max_by_calculus"]);
126 writeln (I_Model.to_string ctxt mits);
128 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
129 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
130 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
131 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
132 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
133 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
134 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
135 0 <= x & x <= 2 * r}])),
136 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
137 if I_Model.to_string ctxt mits
138 = "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])), \n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])), \n(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
139 then () else error "completetest.sml: new behav. in I_Model.complete 1";
144 "----------- specify-phase: low level functions -----------------------------------------";
145 "----------- specify-phase: low level functions -----------------------------------------";
146 "----------- specify-phase: low level functions -----------------------------------------";
147 val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
148 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
149 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
150 "AbleitungBiegelinie dy"];
151 val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
152 val p = e_pos'; val c = [];
153 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(formalise, references)]; (*nxt = Model_Problem*)
155 (*/------------------- check result of CalcTreeTEST ----------------------------------------\*)
156 (*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
157 get_obj g_origin pt (fst p);
158 (*+*)if O_Model.to_string o_model = "[\n" ^
159 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
160 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
161 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
162 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
163 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
164 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
165 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
166 then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
167 (*\------------------- check result of CalcTreeTEST ----------------------------------------/*)
169 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
170 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
171 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
172 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
173 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
174 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
175 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
176 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
178 (*/------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||\*)
179 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
181 (*/------------------- initial check for whole me ------------------------------------------\*)
182 (*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
183 (*+*)val Add_Given "FunktionsVariable x" = nxt''''';
185 (*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
186 Calc.specify_data (pt, p);
187 (*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
188 (*+*)then () else error "initial o_refs CHANGED";
189 (*+*)if O_Model.to_string o_model = "[\n" ^
190 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
191 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
192 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
193 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
194 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
195 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
196 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
197 (*+*)then () else error "initial o_model CHANGED";
198 (*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
199 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
200 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
201 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
202 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]))]"
203 (*+*)then () else error "initial i_pbl CHANGED";
204 (*+*)if I_Model.to_string @{context} i_met = "[]"
205 (*+*)then () else error "initial i_met CHANGED";
206 (*+*)val (_, ["Biegelinien"], _) = spec;
207 (*\------------------- initial check for whole me ------------------------------------------/*)
209 "~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
210 (*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
211 val (pt'''''_', p'''''_') = case
213 Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
214 (*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
215 (*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
216 (*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
217 (*+*)if O_Model.to_string o_model = "[\n" ^
218 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
219 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
220 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
221 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
222 (* these -------vvvvvv must be read from Model_Pattern in *)
223 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
224 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
225 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
226 (*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
227 (*\------------------- check for Step.by_tactic --------------------------------------------/*)
228 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
229 val Applicable.Yes tac' = (*case*)
231 Step.check tac (pt, p) (*of*);
232 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
233 (*if*) Tactic.for_specify tac (*then*);
235 Specify_Step.check tac (ctree, pos);
236 "~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
238 val (o_model''''', _, i_model''''') =
239 Specify_Step.complete_for mID (ctree, pos);
240 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
241 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
242 ...} = Calc.specify_data (ctree, pos);
243 val (dI, _, _) = References.select o_refs refs;
244 val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
245 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
246 val (o_model', ctxt') =
248 O_Model.complete_for m_patt root_model (o_model, ctxt);
249 (*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
250 (*+*)Model_Pattern.to_string m_patt = "[\"" ^
251 "(#Given, (Traegerlaenge, l))\", \"" ^
252 "(#Given, (Streckenlast, q))\", \"" ^
253 "(#Given, (FunktionsVariable, v))\", \"" ^
254 "(#Given, (GleichungsVariablen, vs))\", \"" ^
255 "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
256 "(#Find, (Biegelinie, b))\", \"" ^
257 "(#Relate, (Randbedingungen, s))\"]";
258 (*+*) O_Model.to_string root_model = "[\n" ^ (*.. = o_model for Pos.([], _) *)
259 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
260 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
261 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
262 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
263 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
264 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
265 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
266 (*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
267 "~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
268 val missing = m_patt |> filter_out
269 (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
270 val add = (root_model
272 (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
275 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
276 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
277 |> add_id (* for correct enumeration *)
278 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
279 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
280 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
282 |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
283 |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
284 |> add_id (* for correct enumeration *)
285 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
286 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
288 (*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
289 (*+*)if O_Model.to_string o_model' = "[\n" ^
290 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
291 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
292 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
293 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
294 "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
295 "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
296 "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
297 (*+*)then () else error "O_Model.complete_for: result o_model CHANGED";
298 (*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
300 val thy = ThyC.get_theory dI
301 val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
303 (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
305 "~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
306 (o_model', ctxt', i_model);
308 Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
309 "~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
310 (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
311 (*if*) Tactic.for_specify' tac' (*then*);
312 val ("ok", ([], [], (_, _))) =
314 Step_Specify.by_tactic tac' ptp;
315 "~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
317 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
318 (*NEW*) ...} = Calc.specify_data (pt, pos);
319 (*NEW*) val (dI, _, mID) = References.select o_refs refs;
320 (*NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
321 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
322 (*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
323 (*NEW*) val thy = ThyC.get_theory dI
324 (*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
325 (*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
326 (*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
328 (*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
329 (*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
330 (*+*)O_Model.to_string o_model = "[\n" ^
331 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
332 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
333 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
334 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
335 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
336 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
337 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
338 (* ERROR -------^^^^^^ CORRECTED TO #Given *)
339 (*+*)if I_Model.to_string @{context} meth = "[\n" ^
340 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
341 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
342 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
343 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
344 "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
345 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
346 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
347 (*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
348 (*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
349 (*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
352 val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
353 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
354 (*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
355 "~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
356 (p'''''_', ((pt'''''_', Pos.e_pos'), []));
357 (*if*) Pos.on_calc_end ip (*else*);
358 val (_, probl_id, _) = Calc.references (pt, p);
359 val _ = (*case*) tacis (*of*);
360 (*if*) probl_id = Problem.id_empty (*else*);
362 val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
363 switch_specify_solve p_ (pt, ip);
364 "~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
365 (*if*) Pos.on_specification ([], state_pos) (*then*);
367 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
368 specify_do_next (pt, input_pos);
369 (*/------------------- check result of specify_do_next -------------------------------------\*)
370 (*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
371 (*+*)if O_Model.to_string ooo_mod = "[\n" ^
372 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
373 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
374 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
375 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
376 "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
377 "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
378 "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
379 (*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
380 (*+*)if I_Model.to_string @{context} meth = "[\n" ^
381 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
382 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
383 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
384 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
385 "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
386 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
387 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
388 (*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
389 (*\------------------- check result of specify_do_next -------------------------------------/*)
390 "~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
392 (**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
393 Specify.find_next_step ptp;
394 "~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
395 (*.NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
396 (*.NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
397 (*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
398 val cpI = if pI = Problem.id_empty then pI' else pI;
399 val cmI = if mI = Method.id_empty then mI' else mI;
400 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
401 val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
402 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
403 val mpc = (#ppc o Method.from_store) cmI
404 val Pos.Met = (*case*) p_ (*of*);
405 val NONE = (*case*) find_first (I_Model.is_error o #5) met (*of*);
407 (*/------------------- check within find_next_step -----------------------------------------\*)
408 (*+*)Model_Pattern.to_string (Method.from_store mI' |> #ppc) = "[\"" ^
409 "(#Given, (Traegerlaenge, l))\", \"" ^
410 "(#Given, (Streckenlast, q))\", \"" ^
411 "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
412 "(#Given, (GleichungsVariablen, vs))\", \"" ^
413 "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
414 "(#Find, (Biegelinie, b))\", \"" ^
415 "(#Relate, (Randbedingungen, s))\"]";
416 (*\------------------- check within find_next_step -----------------------------------------/*)
418 (*case*) item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
419 "~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
420 ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
421 (*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
422 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
423 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
424 fun test_subset itm (_, _, _, d, ts) =
425 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
426 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
427 | false_and_not_Sup (_, _, false, _, _) = true
428 | false_and_not_Sup _ = false
429 val v = if itms = [] then 1 else I_Model.max_vt itms
430 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
433 then itms (* because of dsc without dat *)
434 else filter (testi_vt v) itms; (* itms..vat *)
435 val icl = filter false_and_not_Sup vits; (* incomplete *)
437 (*/------------------- check within item_to_add --------------------------------------------\*)
438 (*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values*)
439 "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
440 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
441 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
442 (*+*)then () else error "icl within item_to_add CHANGED";
443 (*+*)if O_Model.to_string vors = "[\n" ^
444 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
445 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
446 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
447 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
448 "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
449 "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
450 "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
451 (*+*)then () else error "vors within item_to_add CHANGED";
452 (*+*)if I_Model.to_string @{context} itms = "[\n" ^
453 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
454 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
455 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
456 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
457 "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. still NOT ,true ,#Given , Cor*)
458 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
459 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
460 (*+*)then () else error "i_model within item_to_add CHANGED";
461 (*\------------------- check within item_to_add --------------------------------------------/*)
463 (*if*) icl = [] (*else*);
464 val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
466 (*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) = ori
467 (*+*)val SOME ("#Given", "FunktionsVariable x") =
470 (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*);
471 "~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
474 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
475 (d, subtract op = (ts_in itm_) ts)) (*return from geti_ct*);
476 "~~~~~ ~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
478 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
480 (*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
482 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
483 ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
484 val ist_ctxt = Ctree.get_loc pt (p, p_)
485 val _ = (*case*) tac (*of*);
488 Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
489 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
490 (tac, (pt, (p, p_')));
492 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
493 Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
494 "~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
495 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
496 (*if*) p_ = Pos.Met (*then*);
497 val (i_model, m_patt) = (met,
498 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
500 val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
502 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
503 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
504 (ctxt, m_field, oris, i_model, m_patt, ct);
505 (*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
506 (*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
508 val ("", (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), [Free ("x", _)]) =
510 O_Model.is_known ctxt m_field o_model t (*of*);
511 "~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
512 val ots = ((distinct op =) o flat o (map #5)) ori
513 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
514 val (d, ts) = Input_Descript.split t
515 val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
516 (*if*) (subtract op = oids ids) <> [] (*else*);
517 (*if*) d = TermC.empty (*else*);
518 (*if*) member op = (map #4 ori) d (*then*);
520 seek_oridts ctxt sel (d, ts) ori;
521 "~~~~~ ~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
522 (ctxt, sel, (d, ts), ori);
524 (*/------------------- check within seek_oridts --------------------------------------------\*)
525 (*+*)val Add_Given "FunktionsVariable x" = tac;
526 (*+*)m_field = "#Given";
527 (*+*)val Const ("Biegelinie.FunktionsVariable", _) = descript;
528 (*+*)val [Free ("x", _)] = vals;
529 (*+*)O_Model.to_string ori = "[\n" ^
530 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
531 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
532 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
533 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
534 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
535 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
536 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
537 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
538 (*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) =
539 (id, vat, m_field', descript', vals')
540 (*\------------------- check within seek_oridts --------------------------------------------/*)
541 (*-------------------- stop step into whole me ----------------------------------------------*)
542 (*\------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||/*)
544 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
545 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
546 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
547 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Model_Problem*)
549 (*/------------------- check entry to me Model_Problem -------------------------------------\*)
550 (*+*)val ([1], Pbl) = p;
551 (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
552 get_obj g_origin pt (fst p);
553 (*+*)if O_Model.to_string o_model = "[\n" ^
554 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
555 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
556 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
558 .. here the O_Model does NOT know, which Method will be chosen,
559 so "belastung_zu_biegelinie q__q v_v id_fun id_abl" is NOT known,
560 "id_fun" and "id_abl" are NOT missing.
562 then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
563 (*\------------------- check entry to me Model_Problem -------------------------------------/*)
565 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
566 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
567 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
568 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
569 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
570 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
572 (*[1], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
573 (*/------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||\*)
574 (*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
575 (*+*)(* by ^^^^^^^^^^^^ "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
577 "~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
579 val ("ok", ([], [], (_, _))) = (*case*)
580 Step.by_tactic tac (pt, p) (*of*);
581 "~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
582 val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
583 (*if*) Tactic.for_specify' tac' (*then*);
585 val ("ok", ([], [], (_, _))) =
586 Step_Specify.by_tactic tac' ptp;
587 (*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
588 (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
589 get_obj g_origin pt (fst p);
590 (*+*)if O_Model.to_string o_model = "[\n" ^
591 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
592 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
593 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
595 .. here the Method has been determined by the user,
596 so "belastung_zu_biegelinie q__q v_v id_fun id_abl" IS KNOWN and,
597 "id_fun" and "id_abl" WOULD BE missing (added by O_Model.).
599 then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method";
600 (*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
601 "~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
603 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
604 (*.NEW*) ...} =Calc.specify_data (pt, pos);
605 (*.NEW*) val (dI, _, mID) = References.select o_refs refs;
606 (*.NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
607 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
608 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
610 (*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
611 (*+*)if mID = ["Biegelinien", "ausBelastung"]
612 (*+*)then () else error "Method [Biegelinien, ausBelastung] CHANGED";
613 (*+*)if Model_Pattern.to_string m_patt = "[\"" ^
614 "(#Given, (Streckenlast, q__q))\", \"" ^
615 "(#Given, (FunktionsVariable, v_v))\", \"" ^
616 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*.. add value from O_Model of root-problem*)
617 "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*.. add value from O_Model of root-problem*)
618 "(#Find, (Funktionen, fun_s))\"]"
619 (*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
620 (*+*)if O_Model.to_string o_model = "[\n" ^
621 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
622 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
623 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
624 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method CHANGED";
625 (*+*)if O_Model.to_string root_model = "[\n" ^
626 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
627 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
628 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
629 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
630 "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
631 "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
632 "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
633 (*+*)then () else error "[Biegelinien, ausBelastung] root O_Model CHANGED";
634 (*+*)if O_Model.to_string o_model' = "[\n" ^ (*.. OK: is value of O_Model.complete_for *)
635 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
636 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
637 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
638 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*.. value from O_Model of root-problem*)
639 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]" (*.. value from O_Model of root-problem*)
640 (* ^^^----- aim at dropping this field *)
641 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY Method CHANGED";
642 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
644 O_Model.complete_for m_patt root_model (o_model, ctxt);
645 "~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
646 (m_patt, root_model, (o_model, ctxt));
647 val missing = m_patt |> filter_out
648 (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
652 (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
655 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
657 |> map (fn (_, b, c, d, e) => (b, c, d, e))
659 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
660 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
661 "~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
663 (*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
665 |> map (fn (_, b, c, d, e) => (b, c, d, e))
667 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
668 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
670 (*/------------------- check within O_Model.complete_for -------------------------------------------\*)
671 (*+*)if O_Model.to_string o_model' = "[\n" ^ (*.. OK: is return from step into *)
672 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
673 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
674 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
675 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^
676 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
677 (* ^^^----- aim at dropping this field *)
678 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY Method CHANGED";
679 (*\------------------- check within O_Model.complete_for -------------------------------------------/*)
681 (*.NEW*) val thy = ThyC.get_theory dI
682 (*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
683 (*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
684 (*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
686 (*+*)if I_Model.to_string @{context} i_model = "[\n" ^
687 "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
688 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
689 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
690 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
691 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
692 (*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED 1";
693 (*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
694 (*+*) Calc.specify_data (pt, pos);
695 (*+*)pos = ([1], Met);
697 ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
698 "~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
699 ("ok", ([], [], (pt, pos)));
700 (* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
701 (* SHOULD BE ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
703 val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
704 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
705 "~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
706 (*.NEW*)(*if*) on_calc_end ip (*else*);
707 (*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
708 (*-"-*) val _ = (*case*) tacis (*of*);
709 (*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
711 (*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
712 switch_specify_solve p_ (pt, ip);
713 "~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
714 (*if*) Pos.on_specification ([], state_pos) (*then*);
716 val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
717 specify_do_next (pt, input_pos);
718 "~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
720 val (_, (p_', tac)) =
721 Specify.find_next_step ptp;
722 "~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
723 val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
724 case Ctree.get_obj I pt p of
725 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
726 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
727 | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"
729 (*+*)O_Model.to_string oris = "[\n" ^
730 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
731 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
732 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
733 "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
734 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
735 (*+*)I_Model.is_complete pbl = true;
736 (*+*)I_Model.to_string @{context} met = "[\n" ^
737 "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
738 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
739 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
740 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
741 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
743 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
744 val cpI = if pI = Problem.id_empty then pI' else pI;
745 val cmI = if mI = Method.id_empty then mI' else mI;
746 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
747 val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
748 val preok = foldl and_ (true, map fst pre);
749 val mpc = (#ppc o Method.from_store) cmI
750 val Pos.Met = (*case*) p_ (*of*);
751 val NONE = (*case*) find_first (is_error o #5) met (*of*);
752 (*val SOME ("#Given", "Biegelinie y") =*)
753 val SOME (fd, ct') = (*case*)
754 item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
756 ("ok", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
757 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
758 ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
759 (*+*)val Add_Given "Biegelinie y" = tac;
760 val ist_ctxt = Ctree.get_loc pt (p, p_)
761 val _ = (*case*) tac (*of*);
763 val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
764 Step_Specify.by_tactic_input tac (pt, (p, p_'))
765 (*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
766 (*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
767 (*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
768 "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
769 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
770 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
771 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
772 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
773 (*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
774 "~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
776 Specify.by_Add_ "#Given" ct ptp;
777 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
778 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
779 (*if*) p_ = Pos.Met (*then*);
780 val (i_model, m_patt) = (met,
781 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
783 val Add (4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
785 check_single ctxt m_field oris i_model m_patt ct (*of*);
787 (*/------------------- check for entry to check_single -------------------------------------\*)
788 (*+*)if O_Model.to_string oris = "[\n" ^
789 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
790 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
791 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
792 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*-------------------^^^^^^^^^^^^^*)
793 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
794 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
795 (*+*)if I_Model.to_string ctxt met = "[\n" ^
796 "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
797 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
798 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
799 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
800 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
801 (*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
802 (*\------------------- check for entry to check_single -------------------------------------/*)
804 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
805 (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
806 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
808 (*+*)val Const ("Biegelinie.Biegelinie", _) $ Free ("y", _) = t;
810 (*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
812 is_known ctxt m_field o_model t (*of*);
813 "~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
814 val ots = ((distinct op =) o flat o (map #5)) ori
815 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
816 val (d, ts) = Input_Descript.split t
817 val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
818 (*if*) (subtract op = oids ids) <> [] (*else*);
819 (*if*) d = TermC.empty (*else*);
820 (*if*) not (subset op = (map typeless ts, map typeless ots)) (*else*);
822 (*case*) O_Model.seek_orits ctxt sel ts ori (*of*);
823 "~~~~~ ~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
825 (*+/---------------- bypass recursion of seek_orits ----------------\*)
826 (*+*)O_Model.to_string oris = "[\n" ^
827 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
828 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
829 "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
830 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
831 (*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
832 (*+\---------------- bypass recursion of seek_orits ----------------/*)
834 (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
836 (*/------------------- check within seek_orits -------------------------------\*)
837 (*+*)if sel = "#Given" andalso sel' = "#Given"
838 (*+*)then () else error "seek_orits Model_Pattern CHANGED";
839 (*BUT: m_field can change from root-Problem to sub-Method --------------------vvv*)
840 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
841 (*+*)if (Problem.from_store ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
842 "(#Given, (Streckenlast, q_q))\", \"" ^
843 "(#Given, (FunktionsVariable, v_v))\", \"" ^
844 "(#Find, (Funktionen, funs'''))\"]"
845 (*+*)then () else error "seek_orits Model_Pattern of Subproblem CHANGED";
846 (* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv -------------------------------------^^^*)
847 (*+*)if (Problem.from_store ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
848 "(#Given, (Traegerlaenge, l_l))\", \"" ^
849 "(#Given, (Streckenlast, q_q))\", \"" ^
850 "(#Find, (Biegelinie, b_b))\", \"" ^ (*-------------------------------------^^^*)
851 "(#Relate, (Randbedingungen, r_b))\"]"
852 (*+*)then () else error "seek_orits Model_Pattern root-problem CHANGED";
853 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
854 (*+*)if (Method.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
855 "(#Given, (Streckenlast, q__q))\", \"" ^
856 "(#Given, (FunktionsVariable, v_v))\", \"" ^
857 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*---------------------------------^^^*)
858 "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
859 "(#Find, (Funktionen, fun_s))\"]"
860 (*+*)then () else error "seek_orits Model_Pattern CHANGED";
861 (*+*)if UnparseC.term d = "Biegelinie"andalso UnparseC.terms ts = "[\"y\"]"
862 (*+*) andalso UnparseC.terms ts' = "[\"y\"]"
864 (*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
865 (*+*) | _ => error "check within seek_orits CHANGED 1")
866 (*+*)else error "check within seek_orits CHANGED 2";
867 (*\------------------- check within seek_orits -------------------------------/*)
868 (*-------------------- stop step into me\<rightarrow>Add_Given "Biegelinie y" --------------------------*)
869 (*\------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||/*)
871 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
872 (*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["Biegelinien", "ausBelastung"]*)
873 (*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("sym_neg_equal_iff_equal", "(?a1 = ?b1) = (- ?a1 = - ?b1)")*)
874 (*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x")*)
875 (*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Subproblem ("Biegelinie", ["named", "integrate", "function"])*)
876 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Model_Problem*)
877 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "functionTerm (- q_0)"*)
878 (*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "integrateBy x"*)
880 (*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
881 if p = ([1, 3], Pbl) andalso
882 f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
883 Given = [Incompl "integrateBy", Correct "functionTerm (- q_0)"],
884 Relate = [], Where = [], With = []})
886 (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
887 else error "specify-phase: low level CHANGED 2";
888 (*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)