1 (* Title: "Minisubpbl/150a-add-given-Maximum.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
5 Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
6 in order not to get lost while working in Test_Some etc,
7 re-introduce ML (*--- step into XXXXX ---*) and Co.
8 and use Sidekick for orientation.
9 Nesting is indicated by /--- //-- ///- at the left margin of the comments.
17 val (_(*example text*),
18 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
19 "Extremum (A = 2 * u * v - u \<up> 2)" ::
20 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
21 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
22 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
23 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
24 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
25 "ErrorBound (\<epsilon> = (0::real))" :: []),
27 ["univariate_calculus", "Optimisation"],
28 ["Optimisation", "by_univariate_calculus"])))
29 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
31 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
34 (*+*)val PblObj {ctxt, ...} = get_obj I pt [];
35 (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
36 (*val Free ("r", TFree ("'a", [])) = Syntax.read_term ctxt "r" ..ERROR until cs.b7a2ad3b3d45*)
37 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
39 val return_me_Model_Problem =
40 me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
41 (*/------------------- step into me Model_Problem ------------------------------------------\\*)
42 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
44 (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
45 case Step.by_tactic tac (pt,p) of
46 ("ok", (_, _, ptp)) => ptp;
48 (*val ("ok", (ts as (_, _, _) :: _, _, _)) = (*case*)*)
49 val return_do_next = (*case*)
50 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
51 val ts = return_do_next |> #2 |> #1 |> hd (* keep for continuing me Model_Problem *)
52 val continue_Model_Problem = (ts, (pt, p)) (* keep for continuing me Model_Problem *);
53 (*//------------------ step into do_next ---------------------------------------------------\\*)
54 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
55 (p, ((pt, e_pos'),[]));
56 val pIopt = get_pblID (pt,ip);
57 (*if*) ip = ([],Res); (* = false*)
58 val _ = (*case*) tacis (*of*);
59 val SOME _ = (*case*) pIopt (*of*);
61 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
62 Step.switch_specify_solve p_ (pt, ip);
63 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
64 (*if*) Pos.on_specification ([], state_pos) (*then*);
66 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
67 Step.specify_do_next (pt, input_pos);
68 (*///----------------- step into specify_do_next -------------------------------------------\\*)
69 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
71 (* val (_, (p_', tac)) =*)
72 val return_find_next_step = (*keep for continuing specify_do_next*)
73 Specify.find_next_step ptp;
74 (*////---------------- step into find_next_step --------------------------------------------\\*)
75 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
76 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
77 spec = refs, ...} = Calc.specify_data (pt, pos);
78 val ctxt = Ctree.get_ctxt pt pos;
79 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
80 (*if*) p_ = Pos.Pbl (*then*);
82 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
83 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
84 = (ctxt, oris, (o_refs, refs), (pbl, met));
85 val cdI = if dI = ThyC.id_empty then dI' else dI;
86 val cpI = if pI = Problem.id_empty then pI' else pI;
87 val cmI = if mI = MethodC.id_empty then mI' else mI;
88 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
89 val {model = mpc, ...} = MethodC.from_store ctxt cmI
90 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
91 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
92 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
93 (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
96 Specify.item_to_add (ThyC.get_theory_PIDE ctxt
97 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
98 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
99 = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
100 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
101 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
102 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
103 fun test_subset itm (_, _, _, d, ts) =
104 (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
105 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
106 | false_and_not_Sup (_, _, false, _, _) = true
107 | false_and_not_Sup _ = false
108 val v = if itms = [] then 1 else I_Model.max_variant itms
109 val vors = if v = 0 then oris else filter (testr_vt v) oris
112 then itms (* because of dsc without dat *)
113 else filter (testi_vt v) itms; (* itms..vat *)
114 val icl = filter false_and_not_Sup vits; (* incomplete *)
115 (*if*) icl = [] (*else*);
117 (*case*) find_first (test_subset (hd icl)) vors (*of*);
118 (*\\\\---------------- step into find_next_step --------------------------------------------//*)
119 (*|||----------------- continuing specify_do_next --------------------------------------------*)
120 val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
122 val ist_ctxt = Ctree.get_loc pt (p, p_)
123 (*+*)val Add_Given "Constants [r = 7]" = tac
127 Step_Specify.by_tactic_input tac (pt, (p, p_'));
128 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
129 (tac, (pt, (p, p_')));
131 Specify.by_Add_ "#Given" ct ptp;
132 "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
134 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
135 val (i_model, m_patt) =
138 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
141 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
143 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
144 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
145 (ctxt, m_field, oris, i_model, m_patt, ct);
146 (*new*) val (t as (descriptor $ _)) = Syntax.read_term ctxt str
148 (*+*)val "Constants [r = 7]" = UnparseC.term_in_ctxt @{context} t;
150 (*new*)val SOME m_field' =
151 (*new*) (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
152 (*new*) (*if*) m_field <> m_field' (*else*);
154 (*+*)val "#Given" = m_field; val "#Given" = m_field'
156 (*new*)val (msg, _, _) =
157 (*new*) (*case*) O_Model.contains ctxt m_field o_model t (*of*);
159 (*+*)val (_, _, _, _, vals) = hd o_model;
160 (*+*)val "Constants [r = 7]" = UnparseC.term_in_ctxt @{context} (@{term Constants} $ (hd vals));
161 (*+*) if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
162 (*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
163 (*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
164 (*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
165 (*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
166 (*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
167 (*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
168 (*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
169 (*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
170 (*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
171 (*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
172 (*+*) = O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
173 (*\\------------------ step into into do_next ----------------------------------------------//*)
175 (*|------------------- continue with me Model_Problem ----------------------------------------*)
176 val (ts, (pt, p)) = continue_Model_Problem;
177 val ("ok", (ts as (_, _, _) :: _, _, _)) = return_do_next
179 val tacis as (_::_) =
181 val (tac, _, _) = last_elem tacis
183 val return = (p, [] : NEW,
184 TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
185 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
186 val (form, _, _) = ME_Misc.pt_extract ctxt ptp
187 val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
188 (*case*) form (*of*);
190 (*+*)val Pos.Pbl = p_;
191 Test_Out.PpcKF ( (Test_Out.Problem [],
192 P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
194 P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
195 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
196 fun coll model [] = model
197 | coll model ((_, _, _, field, itm_) :: itms) =
198 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
200 val gfr = coll P_Model.empty itms;
201 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
202 = (P_Model.empty, itms);
204 (*+*)val 4 = length itms;
205 (*+*)val itm = nth 1 itms;
207 coll P_Model.empty [itm];
208 "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
209 = (P_Model.empty, [itm]);
211 (add_sel_ppc thy field model (item_from_feedback thy itm_));
212 "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
213 = (thy, field, model, (item_from_feedback thy itm_));
215 P_Model.item_from_feedback thy itm_;
216 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
217 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
218 (*\------------------- step into into me Model_Problem -------------------------------------//*)
219 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
221 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Maximum A" = nxt;
222 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
223 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
224 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
225 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;
227 val return_me_Specify_Theory
228 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
230 (*/------------------- step into me Specify_Theory -----------------------------------------\\*)
231 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
232 val ctxt = Ctree.get_ctxt pt p
234 case Step.by_tactic tac (pt, p) of
235 ("ok", (_, _, ptp)) => ptp
237 val ("ok", (ts as (_, _, _) :: _, _, _)) =
239 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
240 (*//------------------ step into do_next ---------------------------------------------------\\*)
241 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
242 = (p, ((pt, Pos.e_pos'), [])) (*of*);
243 (*if*) Pos.on_calc_end ip (*else*);
244 val (_, probl_id, _) = Calc.references (pt, p);
246 (*case*) tacis (*of*);
247 (*if*) probl_id = Problem.id_empty (*else*);
249 Step.switch_specify_solve p_ (pt, ip);
250 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
251 (*if*) Pos.on_specification ([], state_pos) (*then*);
253 Step.specify_do_next (pt, input_pos);
254 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
255 val (_, (p_', tac)) = Specify.find_next_step ptp
256 val ist_ctxt = Ctree.get_loc pt (p, p_);
259 Step_Specify.by_tactic_input tac (pt, (p, p_'));
260 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Problem pI), (pt, pos as (p, _)))
261 = (tac, (pt, (p, p_')));
262 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
263 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
264 (oris, dI, dI', pI', probl, ctxt)
265 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
266 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
267 (*\\------------------ step into do_next ---------------------------------------------------//*)
268 (*\------------------- step into me Specify_Theory -----------------------------------------//*)
269 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
271 val return_me_Specify_Problem (* keep for continuing me *)
272 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
273 (*/------------------- step into me Specify_Problem ----------------------------------------\\*)
274 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
275 val ctxt = Ctree.get_ctxt pt p
277 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
278 (**) val return_by_tactic =(**) (*case*)
279 Step.by_tactic tac (pt, p) (*of*);
280 (*//------------------ step into by_tactic -------------------------------------------------\\*)
281 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
284 Step.check tac (pt, p) (*of*);
285 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
286 (*if*) Tactic.for_specify tac (*then*);
288 Specify_Step.check tac (ctree, pos);
289 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
290 = (tac, (ctree, pos));
291 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
292 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
293 => (oris, dI, pI, dI', pI', itms)
294 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
295 (*\\------------------ step into by_tactic -------------------------------------------------//*)
296 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
299 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
300 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
301 (*if*) Pos.on_calc_end ip (*else*);
302 val (_, probl_id, _) = Calc.references (pt, p);
304 (*case*) tacis (*of*);
305 (*if*) probl_id = Problem.id_empty (*else*);
307 Step.switch_specify_solve p_ (pt, ip);
308 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
309 (*if*) Pos.on_specification ([], state_pos) (*then*);
311 Step.specify_do_next (pt, input_pos);
312 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
313 val (_, (p_', tac)) = Specify.find_next_step ptp
314 val ist_ctxt = Ctree.get_loc pt (p, p_)
318 Step_Specify.by_tactic_input tac (pt, (p, p_'));
319 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
320 = (tac, (pt, (p, p_')));
322 val (o_model, ctxt, i_model) =
323 Specify_Step.complete_for id (pt, pos);
324 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
325 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
326 ...} = Calc.specify_data (ctree, pos);
327 val ctxt = Ctree.get_ctxt ctree pos
328 val (dI, _, _) = References.select_input o_refs refs;
329 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
330 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
331 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
332 val thy = ThyC.get_theory_PIDE ctxt dI
333 val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
334 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
335 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
337 val return_me_Add_Given_FunctionVariable
338 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
339 (*/------------------- step into me Specify_Method -----------------------------------------\\*)
340 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
341 val ctxt = Ctree.get_ctxt pt p
343 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
344 case Step.by_tactic tac (pt, p) of
345 ("ok", (_, _, ptp)) => ptp;
348 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
349 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
350 (*if*) Pos.on_calc_end ip (*else*);
351 val (_, probl_id, _) = Calc.references (pt, p);
353 (*case*) tacis (*of*);
354 (*if*) probl_id = Problem.id_empty (*else*);
356 Step.switch_specify_solve p_ (pt, ip);
357 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
358 (*if*) Pos.on_specification ([], state_pos) (*then*);
360 Step.specify_do_next (pt, input_pos);
361 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
363 val (_, (p_', tac)) =
364 Specify.find_next_step ptp;
365 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
366 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
367 spec = refs, ...} = Calc.specify_data (pt, pos);
368 val ctxt = Ctree.get_ctxt pt pos;
369 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
370 (*if*) p_ = Pos.Pbl (*else*);
372 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
373 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
374 = (ctxt, oris, (o_refs, refs), (pbl, met));
375 val cmI = if mI = MethodC.id_empty then mI' else mI;
376 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
377 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
379 (*case*) find_first (I_Model.is_error o #5) met (*of*);
382 Specify.item_to_add (ThyC.get_theory_PIDE ctxt
383 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
384 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
385 = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
386 (*\------------------- step into me Specify_Method -----------------------------------------//*)
387 val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
390 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
392 nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,
393 but the ***Program*** is not yet perfectly implemented.
394 val (p,_,f,nxt,_,pt) = me nxt p c pt;