4 val e_cterm' = empty_cterm';
7 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
8 (rew_ord':rew_ord',erls,ca)
9 | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
11 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
13 | rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'");
15 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
16 fun from_pblobj_or_detail_thm thm' p pt =
17 let val (pbl,p',rls') = par_pbl_det pt p
19 then let (*val _= writeln("### from_pblobj_or_detail_thm: pbl=true")*)
20 val thy' = get_obj g_domID pt p'
21 val {rew_ord',erls,(*asm_thm,*)...} =
22 get_met (get_obj g_metID pt p')
23 (*val _= writeln("### from_pblobj_or_detail_thm: metID= "^
24 (metID2str(get_obj g_metID pt p')))
25 val _= writeln("### from_pblobj_or_detail_thm: erls= "^erls)*)
26 in ("OK",thy',rew_ord',erls,(*put_asm*)false)
28 else ((*writeln("### from_pblobj_or_detail_thm: pbl=false");*)
29 (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
30 NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
32 let val thy' = get_obj g_domID pt (par_pblobj pt p)
33 val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
34 in ("OK",thy',rew_ord',erls,false) end)
36 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
37 fun from_pblobj_or_detail_calc scrop p pt =
38 (* val (scrop, p, pt) = (op_, p, pt);
40 let val (pbl,p',rls') = par_pbl_det pt p
42 then let val thy' = get_obj g_domID pt p'
43 val {calc = scr_isa_fns,...} =
44 get_met (get_obj g_metID pt p')
45 val opt = assoc (scr_isa_fns, scrop)
47 SOME isa_fn => ("OK",thy',isa_fn)
48 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
50 else (*case assoc(!ruleset', rls') of
51 NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
52 | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
53 (* val SOME rls = assoc(!ruleset', rls');
55 let val thy' = get_obj g_domID pt (par_pblobj pt p);
56 val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
57 in case assoc (scr_isa_fns, scrop) of
58 SOME isa_fn => ("OK",thy',isa_fn)
59 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
62 (*------------------------------------------------------------------*)
64 val op_and = Const ("op &", [bool, bool] ---> bool);
65 (*> (Thm.cterm thy) (op_and $ Free("a",bool) $ Free("b",bool));
66 val it = "a & b" : cterm
68 fun mk_and a b = op_and $ a $ b;
70 (mk_and (Free("a",bool)) (Free("b",bool)));
71 val it = "a & b" : cterm*)
73 fun mk_and [] = HOLogic.true_const
76 let fun mk t' (t::[]) = op_and $ t' $ t
77 | mk t' (t::ts) = mk (op_and $ t' $ t) ts
79 (*> val pred = map (term_of o the o (parse thy))
80 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
81 > (Thm.cterm thy) (mk_and pred);
82 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
87 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
88 fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])
90 | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
91 (e_term, if pred <> Const ("Script.Assumptions",bool)
93 else (map fst) (get_assumptions_ pt (p,Res)))
95 (* val pred = (term_of o the o (parse thy)) pred;
96 val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
97 mk_set thy pt p consts pred;
99 | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =
100 let val (bdv,_) = HOLogic.dest_eq eq;
101 val pred = if pred <> Const ("Script.Assumptions",bool)
103 else (map fst) (get_assumptions_ pt (p,Res))
106 | mk_set thy _ _ l _ =
107 raise error ("check_elementwise: no set "^
108 (Syntax.string_of_term (thy2ctxt thy) l));
109 (*> val consts = str2term "[x=#4]";
110 > val pred = str2term "Assumptions";
111 > val pt = union_asm pt p
112 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
113 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
115 > val (sss,ttt) = mk_set thy pt p consts pred;
116 > (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
117 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
119 val consts = str2term "UniversalList";
120 val pred = str2term "Assumptions";
126 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
127 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
128 val (consts,(bdv,pred)) = (ft,vp);
130 fun check_elementwise thy erls all_results (bdv, asm) =
131 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
133 let val inst_ = map (subst_atomic [sub]) asm
134 in case eval__true thy 1 inst_ [] erls of
135 (asm', true) => ([HOLogic.mk_eq sub], asm')
136 | (_, false) => ([],[])
138 (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^
139 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
140 val c' = isalist2list all_results
141 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
142 val subs = map (pair bdv) c''
143 in if asm = [] then (all_results, [])
144 else ((apfst ((list2isalist bool) o flat)) o
145 (apsnd flat) o split_list o (map check)) subs end;
147 > val all_results = str2term "[x=a+b,x=b,x=3]";
148 > val bdv = str2term "x";
149 > val asm = str2term "(x ~= a) & (x ~= b)";
151 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
152 > term2str t; writeln(terms2str ts);
153 val it = "[x = a + b, x = b, x = c]" : string
154 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
155 ... with appropriate erls this should be:
156 val it = "[x = a + b, x = c]" : string
157 ["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
158 ////// because b ~= b False*)
163 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
164 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
165 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
166 val ct' = "True" : cterm'
168 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
169 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
170 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
171 val ct' = "True" : cterm'
174 > val const = (term_of o the o (parse thy)) "(#3::real)";
175 > val pred' = subst_atomic [(bdv,const)] pred;
178 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
179 > val bdv = (term_of o the o (parse thy)) "(x::real)";
180 > val pred = (term_of o the o (parse thy))
181 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
182 > val ttt = check_elementwise thy consts (bdv, pred);
183 > (Thm.cterm thy) ttt;
184 val it = "[x = #-3, x = #3]" : cterm
186 > val consts = (term_of o the o (parse thy)) "[x = #4]";
187 > val bdv = (term_of o the o (parse thy)) "(x::real)";
188 > val pred = (term_of o the o (parse thy))
189 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
190 > val ttt = check_elementwise thy consts (bdv,pred);
191 > (Thm.cterm thy) ttt;
192 val it = "[x = #4]" : cterm
194 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
195 > val bdv = (term_of o the o (parse thy)) "(x::real)";
196 > val pred = (term_of o the o (parse thy))
197 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
198 > val ttt = check_elementwise thy consts (bdv,pred);
199 > (Thm.cterm thy) ttt;
200 val it = "[]" : cterm*)
203 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
204 fun split_dummy str =
205 let fun scan s' [] = (implode s', "")
206 | scan s' (s::ss) = if s=" " then (implode s', implode ss)
207 else scan (s'@[s]) ss;
208 in ((scan []) o explode) str end;
209 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
210 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
211 > split_dummy "x=-#5//#12";
212 val it = ("x=-#5//#12","") : string * string*)
217 (*.applicability of a tacic wrt. a calc-state (ptree,pos').
218 additionally used by next_tac in the script-interpreter for sequence-tacs.
219 tests for applicability are so expensive, that results (rewrites!)
220 are kept in the return-value of 'type tac_'.
222 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
223 Appl (Init_Proof' (ct', spec))
225 | applicable_in (p,p_) pt Model_Problem =
226 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
227 then Notappl ((tac2str Model_Problem)^
228 " not for pos "^(pos'2str (p,p_)))
229 else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
230 val {ppc,...} = get_pbt pI'
231 val pbl = init_pbl ppc
232 in Appl (Model_Problem' (pI', pbl, [])) end
233 (* val Refine_Tacitly pI = m;
235 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
236 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
237 then Notappl ((tac2str (Refine_Tacitly pI))^
238 " not for pos "^(pos'2str (p,p_)))
239 else (* val Refine_Tacitly pI = m;
241 let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
242 val opt = refine_ori oris pI;
245 Appl (Refine_Tacitly' (pI, pblID,
246 e_domID, e_metID, [](*filled in specify*)))
247 | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
248 " not applicable") end
250 val Refine_Problem pI = m;
252 | applicable_in (p,p_) pt (Refine_Problem pI) =
253 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
254 then Notappl ((tac2str (Refine_Problem pI))^
255 " not for pos "^(pos'2str (p,p_)))
257 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
258 probl=itms, ...}) = get_obj I pt p;
259 val thy = if dI' = e_domID then dI else dI';
260 val rfopt = refine_pbl (assoc_thy thy) pI itms;
262 NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
263 | SOME (rf as (pI',_)) =>
264 (* val SOME (rf as (pI',_)) = rfopt;
267 then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
268 else Appl (Refine_Problem' rf)
271 (*the specify-tacs have cterm' instead term:
272 parse+error here!!!: see appl_add*)
273 | applicable_in (p,p_) pt (Add_Given ct') =
274 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
275 then Notappl ((tac2str (Add_Given ct'))^
276 " not for pos "^(pos'2str (p,p_)))
277 else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
278 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
280 | applicable_in (p,p_) pt (Del_Given ct') =
281 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
282 then Notappl ((tac2str (Del_Given ct'))^
283 " not for pos "^(pos'2str (p,p_)))
284 else Appl (Del_Given' ct')
286 | applicable_in (p,p_) pt (Add_Find ct') =
287 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
288 then Notappl ((tac2str (Add_Find ct'))^
289 " not for pos "^(pos'2str (p,p_)))
290 else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
292 | applicable_in (p,p_) pt (Del_Find ct') =
293 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
294 then Notappl ((tac2str (Del_Find ct'))^
295 " not for pos "^(pos'2str (p,p_)))
296 else Appl (Del_Find' ct')
298 | applicable_in (p,p_) pt (Add_Relation ct') =
299 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
300 then Notappl ((tac2str (Add_Relation ct'))^
301 " not for pos "^(pos'2str (p,p_)))
302 else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
304 | applicable_in (p,p_) pt (Del_Relation ct') =
305 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
306 then Notappl ((tac2str (Del_Relation ct'))^
307 " not for pos "^(pos'2str (p,p_)))
308 else Appl (Del_Relation' ct')
310 | applicable_in (p,p_) pt (Specify_Theory dI) =
311 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
312 then Notappl ((tac2str (Specify_Theory dI))^
313 " not for pos "^(pos'2str (p,p_)))
314 else Appl (Specify_Theory' dI)
315 (* val (p,p_) = p; val Specify_Problem pID = m;
316 val Specify_Problem pID = m;
318 | applicable_in (p,p_) pt (Specify_Problem pID) =
319 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
320 then Notappl ((tac2str (Specify_Problem pID))^
321 " not for pos "^(pos'2str (p,p_)))
323 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
324 probl=itms, ...}) = get_obj I pt p;
325 val thy = assoc_thy (if dI' = e_domID then dI else dI');
326 val {ppc,where_,prls,...} = get_pbt pID;
327 val pbl = if pI'=e_pblID andalso pI=e_pblID
328 then (false, (init_pbl ppc, []))
329 else match_itms_oris thy itms (ppc,where_,prls) oris;
330 in Appl (Specify_Problem' (pID, pbl)) end
331 (* val Specify_Method mID = nxt; val (p,p_) = p;
333 | applicable_in (p,p_) pt (Specify_Method mID) =
334 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
335 then Notappl ((tac2str (Specify_Method mID))^
336 " not for pos "^(pos'2str (p,p_)))
337 else Appl (Specify_Method' (mID,[(*filled in specify*)],
338 [(*filled in specify*)]))
340 | applicable_in (p,p_) pt (Apply_Method mI) =
341 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
342 then Notappl ((tac2str (Apply_Method mI))^
343 " not for pos "^(pos'2str (p,p_)))
344 else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
346 | applicable_in (p,p_) pt (Check_Postcond pI) =
347 if member op = [Pbl,Met] p_
348 then Notappl ((tac2str (Check_Postcond pI))^
349 " not for pos "^(pos'2str (p,p_)))
350 else Appl (Check_Postcond'
351 (pI,(e_term,[(*asm in solve*)])))
352 (* in solve -"- ^^^^^^ gets returnvalue of scr*)
354 (*these are always applicable*)
355 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
356 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
358 (* val m as Rewrite_Inst (subs, thm') = m;
360 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
361 if member op = [Pbl,Met] p_
362 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
365 val pp = par_pblobj pt p;
366 val thy' = (get_obj g_domID pt pp):theory';
367 val thy = assoc_thy thy';
368 val {rew_ord'=ro',erls=erls,...} =
369 get_met (get_obj g_metID pt pp);
370 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
371 Frm => (get_obj g_form pt p, p)
372 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
373 | _ => raise error ("applicable_in: call by "^
376 let val subst = subs2subst thy subs;
377 val subs' = subst2subs' subst;
378 in case rewrite_inst_ thy (assoc_rew_ord ro') erls
379 (*put_asm*)false subst (assoc_thm' thy thm') f of
380 SOME (f',asm) => Appl (
381 Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
382 (*term_of o the o (parse (assoc_thy thy'))*) f,
383 (*(term_of o the o (parse (assoc_thy thy'))*) (f',
384 (*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
385 | NONE => Notappl ((fst thm')^" not applicable") end
386 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
388 (* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
389 val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
391 | applicable_in (p,p_) pt (m as Rewrite thm') =
392 if member op = [Pbl,Met] p_
393 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
395 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
396 val thy = assoc_thy thy';
398 Frm => get_obj g_form pt p
399 | Res => (fst o (get_obj g_result pt)) p
400 | _ => raise error ("applicable_in Rewrite: call by "^
404 ((*writeln("### applicable_in rls'= "^rls');*)
405 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
407 case rewrite_ thy (assoc_rew_ord ro)
408 rls' false (assoc_thm' thy thm') f of
409 SOME (f',asm) => Appl (
410 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
411 | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
415 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
416 if member op = [Pbl,Met] p_
417 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
420 val pp = par_pblobj pt p;
421 val thy' = (get_obj g_domID pt pp):theory';
422 val thy = assoc_thy thy';
423 val {rew_ord'=ro',erls=erls,...} =
424 get_met (get_obj g_metID pt pp);
425 (*val put_asm = true;*)
426 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
427 Frm => (get_obj g_form pt p, p)
428 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
429 | _ => raise error ("applicable_in: call by "^
431 in case rewrite_ thy (assoc_rew_ord ro') erls
432 (*put_asm*)false (assoc_thm' thy thm') f of
433 SOME (f',asm) => Appl (
434 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
435 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
437 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
438 if member op = [Pbl,Met] p_
439 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
442 val pp = par_pblobj pt p;
443 val thy' = (get_obj g_domID pt pp):theory';
444 val thy = assoc_thy thy';
445 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
446 val f = case p_ of Frm => get_obj g_form pt p
447 | Res => (fst o (get_obj g_result pt)) p
448 | _ => raise error ("applicable_in: call by "^
451 let val subst = subs2subst thy subs
452 val subs' = subst2subs' subst
453 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
454 SOME (f',asm) => Appl (
455 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
456 | NONE => Notappl (rls^" not applicable") end
457 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
459 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
460 if member op = [Pbl,Met] p_
461 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
464 val pp = par_pblobj pt p;
465 val thy' = (get_obj g_domID pt pp):theory';
466 val thy = assoc_thy thy';
467 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
468 get_met (get_obj g_metID pt pp);
469 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
470 Frm => (get_obj g_form pt p, p)
471 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
472 | _ => raise error ("applicable_in: call by "^
475 let val subst = subs2subst thy subs;
476 val subs' = subst2subs' subst;
477 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
478 SOME (f',asm) => Appl (
479 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
480 | NONE => Notappl (rls^" not applicable") end
481 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
483 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
484 if member op = [Pbl,Met] p_
485 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
488 val pp = par_pblobj pt p;
489 val thy' = (get_obj g_domID pt pp):theory';
490 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
491 Frm => (get_obj g_form pt p, p)
492 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
493 | _ => raise error ("applicable_in: call by "^
495 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
497 ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*)
498 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
500 | NONE => Notappl (rls^" not applicable") end
502 | applicable_in (p,p_) pt (m as Detail_Set rls) =
503 if member op = [Pbl,Met] p_
504 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
506 let val pp = par_pblobj pt p
507 val thy' = (get_obj g_domID pt pp):theory'
509 Frm => get_obj g_form pt p
510 | Res => (fst o (get_obj g_result pt)) p
511 | _ => raise error ("applicable_in: call by "^
513 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
515 Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
516 | NONE => Notappl (rls^" not applicable") end
519 | applicable_in p pt (End_Ruleset) =
520 raise error ("applicable_in: not impl. for "^
521 (tac2str End_Ruleset))
523 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
525 | applicable_in (p,p_) pt (m as Calculate op_) =
526 if member op = [Pbl,Met] p_
527 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
530 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
532 Frm => get_obj g_form pt p
533 | Res => (fst o (get_obj g_result pt)) p
534 in if msg = "OK" then
535 case calculate_ (assoc_thy thy') isa_fn f of
536 SOME (f', (id, thm)) =>
537 Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
538 | NONE => Notappl ("'calculate "^op_^"' not applicable")
542 (*Substitute combines two different kind of "substitution":
543 (1) subst_atomic: for ?a..?z
544 (2) Pattern.match: for solving equational systems
545 (which raises exn for ?a..?z)*)
546 | applicable_in (p,p_) pt (m as Substitute sube) =
547 if member op = [Pbl,Met] p_
548 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
549 else let val pp = par_pblobj pt p
550 val thy = assoc_thy (get_obj g_domID pt pp)
552 Frm => get_obj g_form pt p
553 | Res => (fst o (get_obj g_result pt)) p
554 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
555 val subte = sube2subte sube
556 val subst = sube2subst thy sube
557 in if foldl and_ (true, map contains_Var subte)
559 then let val f' = subst_atomic subst f
560 in if f = f' then Notappl (sube2str sube^" not applicable")
561 else Appl (Substitute' (subte, f, f'))
564 else case rewrite_terms_ thy (assoc_rew_ord rew_ord')
566 SOME (f', _) => Appl (Substitute' (subte, f, f'))
567 | NONE => Notappl (sube2str sube^" not applicable")
569 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
570 | applicable_in (p,p_) pt (m as Substitute sube) =
571 if member op = [Pbl,Met] p_
572 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
573 else let val pp = par_pblobj pt p
574 val thy = assoc_thy (get_obj g_domID pt pp)
576 Frm => get_obj g_form pt p
577 | Res => (fst o (get_obj g_result pt)) p
578 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
579 val subte = sube2subte sube
580 in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
581 SOME (f', _) => Appl (Substitute' (subte, f, f'))
582 | NONE => Notappl (sube2str sube^" not applicable")
586 | applicable_in p pt (Apply_Assumption cts') =
587 (raise error ("applicable_in: not impl. for "^
588 (tac2str (Apply_Assumption cts'))))
590 (*'logical' applicability wrt. script in locate: Inconsistent?*)
591 | applicable_in (p,p_) pt (m as Take ct') =
592 if member op = [Pbl,Met] p_
593 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
595 let val thy' = get_obj g_domID pt (par_pblobj pt p);
596 in (case parse (assoc_thy thy') ct' of
597 SOME ct => Appl (Take' (term_of ct))
598 | NONE => Notappl ("syntax error in "^ct'))
601 | applicable_in p pt (Take_Inst ct') =
602 raise error ("applicable_in: not impl. for "^
603 (tac2str (Take_Inst ct')))
605 | applicable_in p pt (Group (con, ints)) =
606 raise error ("applicable_in: not impl. for "^
607 (tac2str (Group (con, ints))))
609 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
610 if member op = [Pbl,Met] p_
611 then (*maybe Apply_Method has already been done*)
612 case get_obj g_env pt p of
613 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
614 e_term, [], subpbl domID pblID))
615 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
616 else (*somewhere later in the script*)
617 Appl (Subproblem' ((domID, pblID, e_metID), [],
618 e_term, [], subpbl domID pblID))
620 | applicable_in p pt (End_Subproblem) =
621 raise error ("applicable_in: not impl. for "^
622 (tac2str (End_Subproblem)))
624 | applicable_in p pt (CAScmd ct') =
625 raise error ("applicable_in: not impl. for "^
626 (tac2str (CAScmd ct')))
628 | applicable_in p pt (Split_And) =
629 raise error ("applicable_in: not impl. for "^
630 (tac2str (Split_And)))
631 | applicable_in p pt (Conclude_And) =
632 raise error ("applicable_in: not impl. for "^
633 (tac2str (Conclude_And)))
634 | applicable_in p pt (Split_Or) =
635 raise error ("applicable_in: not impl. for "^
636 (tac2str (Split_Or)))
637 | applicable_in p pt (Conclude_Or) =
638 raise error ("applicable_in: not impl. for "^
639 (tac2str (Conclude_Or)))
641 | applicable_in (p,p_) pt (Begin_Trans) =
643 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
644 (*_____ implizit Take in gen*)
645 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
646 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
647 | _ => raise error ("applicable_in: call by "^
649 val thy' = get_obj g_domID pt (par_pblobj pt p);
650 in (Appl (Begin_Trans' f))
651 handle _ => raise error ("applicable_in: Begin_Trans finds \
652 \syntaxerror in '"^(term2str f)^"'") end
654 (*TODO: check parent branches*)
655 | applicable_in (p,p_) pt (End_Trans) =
656 let val thy' = get_obj g_domID pt (par_pblobj pt p);
658 then Appl (End_Trans' (get_obj g_result pt p))
659 else Notappl "'End_Trans' is not applicable at \
660 \the beginning of a transitive sequence"
661 (*TODO: check parent branches*)
664 | applicable_in p pt (Begin_Sequ) =
665 raise error ("applicable_in: not impl. for "^
666 (tac2str (Begin_Sequ)))
667 | applicable_in p pt (End_Sequ) =
668 raise error ("applicable_in: not impl. for "^
669 (tac2str (End_Sequ)))
670 | applicable_in p pt (Split_Intersect) =
671 raise error ("applicable_in: not impl. for "^
672 (tac2str (Split_Intersect)))
673 | applicable_in p pt (End_Intersect) =
674 raise error ("applicable_in: not impl. for "^
675 (tac2str (End_Intersect)))
676 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
679 val Check_elementwise pred = m;
681 val ((p,p_), Check_elementwise pred) = (p, m);
683 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
684 if member op = [Pbl,Met] p_
685 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
688 val pp = par_pblobj pt p;
689 val thy' = (get_obj g_domID pt pp):theory';
690 val thy = assoc_thy thy'
691 val metID = (get_obj g_metID pt pp)
692 val {crls,...} = get_met metID
693 (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls)
694 val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*)
695 (*val erl = the (assoc'(!ruleset',crls))*)
696 val (f,asm) = case p_ of
697 Frm => (get_obj g_form pt p , [])
698 | Res => get_obj g_result pt p;
699 (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*)
700 val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
701 (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^
702 pair2str(term2str v,term2str p))*)
704 Const ("List.list.Cons",_) $ _ $ _ =>
705 Appl (Check_elementwise'
707 ((*writeln("### applicable_in Check_elementwise: --> "^
708 (res2str (check_elementwise thy crls f vp)));*)
709 check_elementwise thy crls f vp)))
710 | Const ("Tools.UniversalList",_) =>
711 Appl (Check_elementwise' (f, pred, (f,asm)))
712 | Const ("List.list.Nil",_) =>
713 (*Notappl "not applicable to empty list" 3.6.03*)
714 Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
715 | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
718 | applicable_in (p,p_) pt Or_to_List =
719 if member op = [Pbl,Met] p_
720 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
723 val pp = par_pblobj pt p;
724 val thy' = (get_obj g_domID pt pp):theory';
725 val thy = assoc_thy thy';
727 Frm => get_obj g_form pt p
728 | Res => (fst o (get_obj g_result pt)) p;
729 in (let val ls = or2list f
730 in Appl (Or_to_List' (f, ls)) end)
731 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
734 | applicable_in p pt (Collect_Trues) =
735 raise error ("applicable_in: not impl. for "^
736 (tac2str (Collect_Trues)))
738 | applicable_in p pt (Empty_Tac) =
739 Notappl "Empty_Tac is not applicable"
741 | applicable_in (p,p_) pt (Tac id) =
743 val pp = par_pblobj pt p;
744 val thy' = (get_obj g_domID pt pp):theory';
745 val thy = assoc_thy thy';
747 Frm => get_obj g_form pt p
748 | Res => (fst o (get_obj g_result pt)) p;
750 "subproblem_equation_dummy" =>
752 then Appl (Tac_ (thy, term2str f, id,
753 "subproblem_equation_dummy ("^(term2str f)^")"))
754 else Notappl "applicable only to equations made explicit"
755 | "solve_equation_dummy" =>
756 let (*val _= writeln("### applicable_in: solve_equation_dummy: f= "
758 val (id',f') = split_dummy (term2str f);
759 (*val _= writeln("### applicable_in: f'= "^f');*)
760 (*val _= (term_of o the o (parse thy)) f';*)
761 (*val _= writeln"### applicable_in: solve_equation_dummy";*)
762 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
763 else if is_expliceq ((term_of o the o (parse thy)) f')
764 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
765 else error ("applicable_in: f= " ^ f') end
766 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
768 | applicable_in p pt End_Proof' = Appl End_Proof''
770 | applicable_in _ _ m =
771 raise error ("applicable_in called for "^(tac2str m));
774 fun tac2tac_ pt p m =
775 case applicable_in p pt m of
777 | Notappl _ => raise error ("tac2mstp': fails with"^