intermed. test/../integrate.sml in -- me method [diff,integration] --
removed last error by
find . -type f -exec sed -i s/"\"Isac.thy\""/"\"Isac\""/g {} \;
find . -type f -exec sed -i s/" Isac.thy"/" (theory \"Isac\")"/g {} \;
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
7 val e_cterm' = empty_cterm';
10 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
11 (rew_ord':rew_ord',erls,ca)
12 | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
14 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
16 | rew_info rls = error ("rew_info called with '"^rls2str rls^"'");
18 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
19 fun from_pblobj_or_detail_thm thm' p pt =
20 let val (pbl,p',rls') = par_pbl_det pt p
22 then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)
23 val thy' = get_obj g_domID pt p'
24 val {rew_ord',erls,(*asm_thm,*)...} =
25 get_met (get_obj g_metID pt p')
26 (*val _= tracing("### from_pblobj_or_detail_thm: metID= "^
27 (metID2str(get_obj g_metID pt p')))
28 val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
29 in ("OK",thy',rew_ord',erls,(*put_asm*)false)
31 else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)
32 (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
33 NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
35 let val thy' = get_obj g_domID pt (par_pblobj pt p)
36 val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
37 in ("OK",thy',rew_ord',erls,false) end)
39 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
40 fun from_pblobj_or_detail_calc scrop p pt =
41 (* val (scrop, p, pt) = (op_, p, pt);
43 let val (pbl,p',rls') = par_pbl_det pt p
45 then let val thy' = get_obj g_domID pt p'
46 val {calc = scr_isa_fns,...} =
47 get_met (get_obj g_metID pt p')
48 val opt = assoc (scr_isa_fns, scrop)
50 SOME isa_fn => ("OK",thy',isa_fn)
51 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
53 else (*case assoc(!ruleset', rls') of
54 NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
55 | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
56 (* val SOME rls = assoc(!ruleset', rls');
58 let val thy' = get_obj g_domID pt (par_pblobj pt p);
59 val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
60 in case assoc (scr_isa_fns, scrop) of
61 SOME isa_fn => ("OK",thy',isa_fn)
62 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
65 (*------------------------------------------------------------------*)
67 val op_and = Const ("op &", [bool, bool] ---> bool);
68 (*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
69 val it = "a & b" : cterm
71 fun mk_and a b = op_and $ a $ b;
73 (mk_and (Free("a",bool)) (Free("b",bool)));
74 val it = "a & b" : cterm*)
76 fun mk_and [] = HOLogic.true_const
79 let fun mk t' (t::[]) = op_and $ t' $ t
80 | mk t' (t::ts) = mk (op_and $ t' $ t) ts
82 (*> val pred = map (term_of o the o (parse thy))
83 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
84 > (cterm_of thy) (mk_and pred);
85 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
90 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
91 fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])
93 | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
94 (e_term, if pred <> Const ("Script.Assumptions",bool)
96 else (map fst) (get_assumptions_ pt (p,Res)))
98 (* val pred = (term_of o the o (parse thy)) pred;
99 val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
100 mk_set thy pt p consts pred;
102 | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =
103 let val (bdv,_) = HOLogic.dest_eq eq;
104 val pred = if pred <> Const ("Script.Assumptions",bool)
106 else (map fst) (get_assumptions_ pt (p,Res))
109 | mk_set thy _ _ l _ =
110 error ("check_elementwise: no set "^
111 (Syntax.string_of_term (thy2ctxt thy) l));
112 (*> val consts = str2term "[x=#4]";
113 > val pred = str2term "Assumptions";
114 > val pt = union_asm pt p
115 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
116 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
118 > val (sss,ttt) = mk_set thy pt p consts pred;
119 > (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
120 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
122 val consts = str2term "UniversalList";
123 val pred = str2term "Assumptions";
129 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
130 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
131 val (consts,(bdv,pred)) = (ft,vp);
133 fun check_elementwise thy erls all_results (bdv, asm) =
134 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
136 let val inst_ = map (subst_atomic [sub]) asm
137 in case eval__true thy 1 inst_ [] erls of
138 (asm', true) => ([HOLogic.mk_eq sub], asm')
139 | (_, false) => ([],[])
141 (*val _= tracing("### check_elementwise: res= "^(term2str all_results)^
142 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
143 val c' = isalist2list all_results
144 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
145 val subs = map (pair bdv) c''
146 in if asm = [] then (all_results, [])
147 else ((apfst ((list2isalist bool) o flat)) o
148 (apsnd flat) o split_list o (map check)) subs end;
150 > val all_results = str2term "[x=a+b,x=b,x=3]";
151 > val bdv = str2term "x";
152 > val asm = str2term "(x ~= a) & (x ~= b)";
154 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
155 > term2str t; tracing(terms2str ts);
156 val it = "[x = a + b, x = b, x = c]" : string
157 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
158 ... with appropriate erls this should be:
159 val it = "[x = a + b, x = c]" : string
160 ["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
161 ////// because b ~= b False*)
166 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
167 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
168 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
169 val ct' = "True" : cterm'
171 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
172 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
173 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
174 val ct' = "True" : cterm'
177 > val const = (term_of o the o (parse thy)) "(#3::real)";
178 > val pred' = subst_atomic [(bdv,const)] pred;
181 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
182 > val bdv = (term_of o the o (parse thy)) "(x::real)";
183 > val pred = (term_of o the o (parse thy))
184 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
185 > val ttt = check_elementwise thy consts (bdv, pred);
186 > (cterm_of thy) ttt;
187 val it = "[x = #-3, x = #3]" : cterm
189 > val consts = (term_of o the o (parse thy)) "[x = #4]";
190 > val bdv = (term_of o the o (parse thy)) "(x::real)";
191 > val pred = (term_of o the o (parse thy))
192 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
193 > val ttt = check_elementwise thy consts (bdv,pred);
194 > (cterm_of thy) ttt;
195 val it = "[x = #4]" : cterm
197 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
198 > val bdv = (term_of o the o (parse thy)) "(x::real)";
199 > val pred = (term_of o the o (parse thy))
200 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
201 > val ttt = check_elementwise thy consts (bdv,pred);
202 > (cterm_of thy) ttt;
203 val it = "[]" : cterm*)
206 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
207 fun split_dummy str =
208 let fun scan s' [] = (implode s', "")
209 | scan s' (s::ss) = if s=" " then (implode s', implode ss)
210 else scan (s'@[s]) ss;
211 in ((scan []) o explode) str end;
212 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
213 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
214 > split_dummy "x=-#5//#12";
215 val it = ("x=-#5//#12","") : string * string*)
220 (*.applicability of a tacic wrt. a calc-state (ptree,pos').
221 additionally used by next_tac in the script-interpreter for sequence-tacs.
222 tests for applicability are so expensive, that results (rewrites!)
223 are kept in the return-value of 'type tac_'.
225 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
226 Appl (Init_Proof' (ct', spec))
228 | applicable_in (p,p_) pt Model_Problem =
229 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
230 then Notappl ((tac2str Model_Problem)^
231 " not for pos "^(pos'2str (p,p_)))
232 else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
233 val {ppc,...} = get_pbt pI'
234 val pbl = init_pbl ppc
235 in Appl (Model_Problem' (pI', pbl, [])) end
236 (* val Refine_Tacitly pI = m;
238 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
239 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
240 then Notappl ((tac2str (Refine_Tacitly pI))^
241 " not for pos "^(pos'2str (p,p_)))
242 else (* val Refine_Tacitly pI = m;
244 let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
245 val opt = refine_ori oris pI;
248 Appl (Refine_Tacitly' (pI, pblID,
249 e_domID, e_metID, [](*filled in specify*)))
250 | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
251 " not applicable") end
253 val Refine_Problem pI = m;
255 | applicable_in (p,p_) pt (Refine_Problem pI) =
256 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
257 then Notappl ((tac2str (Refine_Problem pI))^
258 " not for pos "^(pos'2str (p,p_)))
260 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
261 probl=itms, ...}) = get_obj I pt p;
262 val thy = if dI' = e_domID then dI else dI';
263 val rfopt = refine_pbl (assoc_thy thy) pI itms;
265 NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
266 | SOME (rf as (pI',_)) =>
267 (* val SOME (rf as (pI',_)) = rfopt;
270 then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
271 else Appl (Refine_Problem' rf)
274 (*the specify-tacs have cterm' instead term:
275 parse+error here!!!: see appl_add*)
276 | applicable_in (p,p_) pt (Add_Given ct') =
277 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
278 then Notappl ((tac2str (Add_Given ct'))^
279 " not for pos "^(pos'2str (p,p_)))
280 else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
281 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
283 | applicable_in (p,p_) pt (Del_Given ct') =
284 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
285 then Notappl ((tac2str (Del_Given ct'))^
286 " not for pos "^(pos'2str (p,p_)))
287 else Appl (Del_Given' ct')
289 | applicable_in (p,p_) pt (Add_Find ct') =
290 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
291 then Notappl ((tac2str (Add_Find ct'))^
292 " not for pos "^(pos'2str (p,p_)))
293 else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
295 | applicable_in (p,p_) pt (Del_Find ct') =
296 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
297 then Notappl ((tac2str (Del_Find ct'))^
298 " not for pos "^(pos'2str (p,p_)))
299 else Appl (Del_Find' ct')
301 | applicable_in (p,p_) pt (Add_Relation ct') =
302 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
303 then Notappl ((tac2str (Add_Relation ct'))^
304 " not for pos "^(pos'2str (p,p_)))
305 else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
307 | applicable_in (p,p_) pt (Del_Relation ct') =
308 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
309 then Notappl ((tac2str (Del_Relation ct'))^
310 " not for pos "^(pos'2str (p,p_)))
311 else Appl (Del_Relation' ct')
313 | applicable_in (p,p_) pt (Specify_Theory dI) =
314 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
315 then Notappl ((tac2str (Specify_Theory dI))^
316 " not for pos "^(pos'2str (p,p_)))
317 else Appl (Specify_Theory' dI)
318 (* val (p,p_) = p; val Specify_Problem pID = m;
319 val Specify_Problem pID = m;
321 | applicable_in (p,p_) pt (Specify_Problem pID) =
322 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
323 then Notappl ((tac2str (Specify_Problem pID))^
324 " not for pos "^(pos'2str (p,p_)))
326 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
327 probl=itms, ...}) = get_obj I pt p;
328 val thy = assoc_thy (if dI' = e_domID then dI else dI');
329 val {ppc,where_,prls,...} = get_pbt pID;
330 val pbl = if pI'=e_pblID andalso pI=e_pblID
331 then (false, (init_pbl ppc, []))
332 else match_itms_oris thy itms (ppc,where_,prls) oris;
333 in Appl (Specify_Problem' (pID, pbl)) end
334 (* val Specify_Method mID = nxt; val (p,p_) = p;
336 | applicable_in (p,p_) pt (Specify_Method mID) =
337 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
338 then Notappl ((tac2str (Specify_Method mID))^
339 " not for pos "^(pos'2str (p,p_)))
340 else Appl (Specify_Method' (mID,[(*filled in specify*)],
341 [(*filled in specify*)]))
343 | applicable_in (p,p_) pt (Apply_Method mI) =
344 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
345 then Notappl ((tac2str (Apply_Method mI))^
346 " not for pos "^(pos'2str (p,p_)))
347 else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
349 | applicable_in (p,p_) pt (Check_Postcond pI) =
350 if member op = [Pbl,Met] p_
351 then Notappl ((tac2str (Check_Postcond pI))^
352 " not for pos "^(pos'2str (p,p_)))
353 else Appl (Check_Postcond'
354 (pI,(e_term,[(*asm in solve*)])))
355 (* in solve -"- ^^^^^^ gets returnvalue of scr*)
357 (*these are always applicable*)
358 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
359 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
361 (* val m as Rewrite_Inst (subs, thm') = m;
363 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
364 if member op = [Pbl,Met] p_
365 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
368 val pp = par_pblobj pt p;
369 val thy' = (get_obj g_domID pt pp):theory';
370 val thy = assoc_thy thy';
371 val {rew_ord'=ro',erls=erls,...} =
372 get_met (get_obj g_metID pt pp);
373 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
374 Frm => (get_obj g_form pt p, p)
375 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
376 | _ => error ("applicable_in: call by "^
379 let val subst = subs2subst thy subs;
380 val subs' = subst2subs' subst;
381 in case rewrite_inst_ thy (assoc_rew_ord ro') erls
382 (*put_asm*)false subst (assoc_thm' thy thm') f of
383 SOME (f',asm) => Appl (
384 Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
385 (*term_of o the o (parse (assoc_thy thy'))*) f,
386 (*(term_of o the o (parse (assoc_thy thy'))*) (f',
387 (*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
388 | NONE => Notappl ((fst thm')^" not applicable") end
389 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
391 (* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
392 val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
394 | applicable_in (p,p_) pt (m as Rewrite thm') =
395 if member op = [Pbl,Met] p_
396 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
398 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
399 val thy = assoc_thy thy';
401 Frm => get_obj g_form pt p
402 | Res => (fst o (get_obj g_result pt)) p
403 | _ => error ("applicable_in Rewrite: call by "^
407 ((*tracing("### applicable_in rls'= "^rls');*)
408 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
410 case rewrite_ thy (assoc_rew_ord ro)
411 rls' false (assoc_thm' thy thm') f of
412 SOME (f',asm) => Appl (
413 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
414 | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
418 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
419 if member op = [Pbl,Met] p_
420 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
423 val pp = par_pblobj pt p;
424 val thy' = (get_obj g_domID pt pp):theory';
425 val thy = assoc_thy thy';
426 val {rew_ord'=ro',erls=erls,...} =
427 get_met (get_obj g_metID pt pp);
428 (*val put_asm = true;*)
429 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
430 Frm => (get_obj g_form pt p, p)
431 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
432 | _ => error ("applicable_in: call by "^
434 in case rewrite_ thy (assoc_rew_ord ro') erls
435 (*put_asm*)false (assoc_thm' thy thm') f of
436 SOME (f',asm) => Appl (
437 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
438 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
440 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
441 if member op = [Pbl,Met] p_
442 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
445 val pp = par_pblobj pt p;
446 val thy' = (get_obj g_domID pt pp):theory';
447 val thy = assoc_thy thy';
448 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
449 val f = case p_ of Frm => get_obj g_form pt p
450 | Res => (fst o (get_obj g_result pt)) p
451 | _ => error ("applicable_in: call by "^
454 let val subst = subs2subst thy subs
455 val subs' = subst2subs' subst
456 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
457 SOME (f',asm) => Appl (
458 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
459 | NONE => Notappl (rls^" not applicable") end
460 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
462 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
463 if member op = [Pbl,Met] p_
464 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
467 val pp = par_pblobj pt p;
468 val thy' = (get_obj g_domID pt pp):theory';
469 val thy = assoc_thy thy';
470 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
471 get_met (get_obj g_metID pt pp);
472 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
473 Frm => (get_obj g_form pt p, p)
474 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
475 | _ => error ("applicable_in: call by "^
478 let val subst = subs2subst thy subs;
479 val subs' = subst2subs' subst;
480 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
481 SOME (f',asm) => Appl (
482 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
483 | NONE => Notappl (rls^" not applicable") end
484 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
486 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
487 if member op = [Pbl,Met] p_
488 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
491 val pp = par_pblobj pt p;
492 val thy' = (get_obj g_domID pt pp):theory';
493 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
494 Frm => (get_obj g_form pt p, p)
495 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
496 | _ => error ("applicable_in: call by "^
498 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
500 ((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
501 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
503 | NONE => Notappl (rls^" not applicable") end
505 | applicable_in (p,p_) pt (m as Detail_Set rls) =
506 if member op = [Pbl,Met] p_
507 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
509 let val pp = par_pblobj pt p
510 val thy' = (get_obj g_domID pt pp):theory'
512 Frm => get_obj g_form pt p
513 | Res => (fst o (get_obj g_result pt)) p
514 | _ => error ("applicable_in: call by "^
516 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
518 Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
519 | NONE => Notappl (rls^" not applicable") end
522 | applicable_in p pt (End_Ruleset) =
523 error ("applicable_in: not impl. for "^
524 (tac2str End_Ruleset))
526 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
528 | applicable_in (p,p_) pt (m as Calculate op_) =
529 if member op = [Pbl,Met] p_
530 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
533 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
535 Frm => get_obj g_form pt p
536 | Res => (fst o (get_obj g_result pt)) p
537 in if msg = "OK" then
538 case calculate_ (assoc_thy thy') isa_fn f of
539 SOME (f', (id, thm)) =>
540 Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
541 | NONE => Notappl ("'calculate "^op_^"' not applicable")
545 (*Substitute combines two different kind of "substitution":
546 (1) subst_atomic: for ?a..?z
547 (2) Pattern.match: for solving equational systems
548 (which raises exn for ?a..?z)*)
549 | applicable_in (p,p_) pt (m as Substitute sube) =
550 if member op = [Pbl,Met] p_
551 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
552 else let val pp = par_pblobj pt p
553 val thy = assoc_thy (get_obj g_domID pt pp)
555 Frm => get_obj g_form pt p
556 | Res => (fst o (get_obj g_result pt)) p
557 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
558 val subte = sube2subte sube
559 val subst = sube2subst thy sube
560 in if foldl and_ (true, map contains_Var subte)
562 then let val f' = subst_atomic subst f
563 in if f = f' then Notappl (sube2str sube^" not applicable")
564 else Appl (Substitute' (subte, f, f'))
567 else case rewrite_terms_ thy (assoc_rew_ord rew_ord')
569 SOME (f', _) => Appl (Substitute' (subte, f, f'))
570 | NONE => Notappl (sube2str sube^" not applicable")
572 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
573 | applicable_in (p,p_) pt (m as Substitute sube) =
574 if member op = [Pbl,Met] p_
575 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
576 else let val pp = par_pblobj pt p
577 val thy = assoc_thy (get_obj g_domID pt pp)
579 Frm => get_obj g_form pt p
580 | Res => (fst o (get_obj g_result pt)) p
581 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
582 val subte = sube2subte sube
583 in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
584 SOME (f', _) => Appl (Substitute' (subte, f, f'))
585 | NONE => Notappl (sube2str sube^" not applicable")
589 | applicable_in p pt (Apply_Assumption cts') =
590 (error ("applicable_in: not impl. for "^
591 (tac2str (Apply_Assumption cts'))))
593 (*'logical' applicability wrt. script in locate: Inconsistent?*)
594 | applicable_in (p,p_) pt (m as Take ct') =
595 if member op = [Pbl,Met] p_
596 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
598 let val thy' = get_obj g_domID pt (par_pblobj pt p);
599 in (case parse (assoc_thy thy') ct' of
600 SOME ct => Appl (Take' (term_of ct))
601 | NONE => Notappl ("syntax error in "^ct'))
604 | applicable_in p pt (Take_Inst ct') =
605 error ("applicable_in: not impl. for "^
606 (tac2str (Take_Inst ct')))
608 | applicable_in p pt (Group (con, ints)) =
609 error ("applicable_in: not impl. for "^
610 (tac2str (Group (con, ints))))
612 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
613 if member op = [Pbl,Met] p_
614 then (*maybe Apply_Method has already been done*)
615 case get_obj g_env pt p of
616 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
617 e_term, [], subpbl domID pblID))
618 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
619 else (*somewhere later in the script*)
620 Appl (Subproblem' ((domID, pblID, e_metID), [],
621 e_term, [], subpbl domID pblID))
623 | applicable_in p pt (End_Subproblem) =
624 error ("applicable_in: not impl. for "^
625 (tac2str (End_Subproblem)))
627 | applicable_in p pt (CAScmd ct') =
628 error ("applicable_in: not impl. for "^
629 (tac2str (CAScmd ct')))
631 | applicable_in p pt (Split_And) =
632 error ("applicable_in: not impl. for "^
633 (tac2str (Split_And)))
634 | applicable_in p pt (Conclude_And) =
635 error ("applicable_in: not impl. for "^
636 (tac2str (Conclude_And)))
637 | applicable_in p pt (Split_Or) =
638 error ("applicable_in: not impl. for "^
639 (tac2str (Split_Or)))
640 | applicable_in p pt (Conclude_Or) =
641 error ("applicable_in: not impl. for "^
642 (tac2str (Conclude_Or)))
644 | applicable_in (p,p_) pt (Begin_Trans) =
646 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
647 (*_____ implizit Take in gen*)
648 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
649 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
650 | _ => error ("applicable_in: call by "^
652 val thy' = get_obj g_domID pt (par_pblobj pt p);
653 in (Appl (Begin_Trans' f))
654 handle _ => error ("applicable_in: Begin_Trans finds \
655 \syntaxerror in '"^(term2str f)^"'") end
657 (*TODO: check parent branches*)
658 | applicable_in (p,p_) pt (End_Trans) =
659 let val thy' = get_obj g_domID pt (par_pblobj pt p);
661 then Appl (End_Trans' (get_obj g_result pt p))
662 else Notappl "'End_Trans' is not applicable at \
663 \the beginning of a transitive sequence"
664 (*TODO: check parent branches*)
667 | applicable_in p pt (Begin_Sequ) =
668 error ("applicable_in: not impl. for "^
669 (tac2str (Begin_Sequ)))
670 | applicable_in p pt (End_Sequ) =
671 error ("applicable_in: not impl. for "^
672 (tac2str (End_Sequ)))
673 | applicable_in p pt (Split_Intersect) =
674 error ("applicable_in: not impl. for "^
675 (tac2str (Split_Intersect)))
676 | applicable_in p pt (End_Intersect) =
677 error ("applicable_in: not impl. for "^
678 (tac2str (End_Intersect)))
679 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
682 val Check_elementwise pred = m;
684 val ((p,p_), Check_elementwise pred) = (p, m);
686 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
687 if member op = [Pbl,Met] p_
688 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
691 val pp = par_pblobj pt p;
692 val thy' = (get_obj g_domID pt pp):theory';
693 val thy = assoc_thy thy'
694 val metID = (get_obj g_metID pt pp)
695 val {crls,...} = get_met metID
696 (*val _=tracing("### applicable_in Check_elementwise: crls= "^crls)
697 val _=tracing("### applicable_in Check_elementwise: pred= "^pred)*)
698 (*val erl = the (assoc'(!ruleset',crls))*)
699 val (f,asm) = case p_ of
700 Frm => (get_obj g_form pt p , [])
701 | Res => get_obj g_result pt p;
702 (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
703 val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
704 (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
705 pair2str(term2str v,term2str p))*)
707 Const ("List.list.Cons",_) $ _ $ _ =>
708 Appl (Check_elementwise'
710 ((*tracing("### applicable_in Check_elementwise: --> "^
711 (res2str (check_elementwise thy crls f vp)));*)
712 check_elementwise thy crls f vp)))
713 | Const ("Tools.UniversalList",_) =>
714 Appl (Check_elementwise' (f, pred, (f,asm)))
715 | Const ("List.list.Nil",_) =>
716 (*Notappl "not applicable to empty list" 3.6.03*)
717 Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
718 | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
721 | applicable_in (p,p_) pt Or_to_List =
722 if member op = [Pbl,Met] p_
723 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
726 val pp = par_pblobj pt p;
727 val thy' = (get_obj g_domID pt pp):theory';
728 val thy = assoc_thy thy';
730 Frm => get_obj g_form pt p
731 | Res => (fst o (get_obj g_result pt)) p;
732 in (let val ls = or2list f
733 in Appl (Or_to_List' (f, ls)) end)
734 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
737 | applicable_in p pt (Collect_Trues) =
738 error ("applicable_in: not impl. for "^
739 (tac2str (Collect_Trues)))
741 | applicable_in p pt (Empty_Tac) =
742 Notappl "Empty_Tac is not applicable"
744 | applicable_in (p,p_) pt (Tac id) =
746 val pp = par_pblobj pt p;
747 val thy' = (get_obj g_domID pt pp):theory';
748 val thy = assoc_thy thy';
750 Frm => get_obj g_form pt p
751 | Res => (fst o (get_obj g_result pt)) p;
753 "subproblem_equation_dummy" =>
755 then Appl (Tac_ (thy, term2str f, id,
756 "subproblem_equation_dummy ("^(term2str f)^")"))
757 else Notappl "applicable only to equations made explicit"
758 | "solve_equation_dummy" =>
759 let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
761 val (id',f') = split_dummy (term2str f);
762 (*val _= tracing("### applicable_in: f'= "^f');*)
763 (*val _= (term_of o the o (parse thy)) f';*)
764 (*val _= tracing"### applicable_in: solve_equation_dummy";*)
765 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
766 else if is_expliceq ((term_of o the o (parse thy)) f')
767 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
768 else error ("applicable_in: f= " ^ f') end
769 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
771 | applicable_in p pt End_Proof' = Appl End_Proof''
773 | applicable_in _ _ m =
774 error ("applicable_in called for "^(tac2str m));
777 fun tac2tac_ pt p m =
778 case applicable_in p pt m of
780 | Notappl _ => error ("tac2mstp': fails with"^