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 (*val put_asm = (fst thm') mem (map fst asm_thm);*)
35 in ("OK",thy',rew_ord',erls,(*put_asm*)false) end)
37 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
38 fun from_pblobj_or_detail_calc scrop p pt =
39 (* val (scrop, p, pt) = (op_, p, pt);
41 let val (pbl,p',rls') = par_pbl_det pt p
43 then let val thy' = get_obj g_domID pt p'
44 val {calc = scr_isa_fns,...} =
45 get_met (get_obj g_metID pt p')
46 val opt = assoc (scr_isa_fns, scrop)
48 SOME isa_fn => ("OK",thy',isa_fn)
49 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
51 else (*case assoc(!ruleset', rls') of
52 NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
53 | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
54 (* val SOME rls = assoc(!ruleset', rls');
56 let val thy' = get_obj g_domID pt (par_pblobj pt p);
57 val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
58 in case assoc (scr_isa_fns, scrop) of
59 SOME isa_fn => ("OK",thy',isa_fn)
60 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
63 (*------------------------------------------------------------------*)
65 val op_and = Const ("op &", [bool, bool] ---> bool);
66 (*> cterm_of (sign_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
67 val it = "a & b" : cterm
69 fun mk_and a b = op_and $ a $ b;
70 (*> cterm_of (sign_of thy)
71 (mk_and (Free("a",bool)) (Free("b",bool)));
72 val it = "a & b" : cterm*)
74 fun mk_and [] = HOLogic.true_const
77 let fun mk t' (t::[]) = op_and $ t' $ t
78 | mk t' (t::ts) = mk (op_and $ t' $ t) ts
80 (*> val pred = map (term_of o the o (parse thy))
81 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
82 > cterm_of (sign_of thy) (mk_and pred);
83 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
88 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
89 fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])
91 | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
92 (e_term, if pred <> Const ("Script.Assumptions",bool)
94 else (map fst) (get_assumptions_ pt (p,Res)))
96 (* val pred = (term_of o the o (parse thy)) pred;
97 val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
98 mk_set thy pt p consts pred;
100 | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =
101 let val (bdv,_) = HOLogic.dest_eq eq;
102 val pred = if pred <> Const ("Script.Assumptions",bool)
104 else (map fst) (get_assumptions_ pt (p,Res))
107 | mk_set thy _ _ l _ =
108 raise error ("check_elementwise: no set "^
109 (Sign.string_of_term (sign_of thy) l));
110 (*> val consts = str2term "[x=#4]";
111 > val pred = str2term "Assumptions";
112 > val pt = union_asm pt p
113 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
114 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
116 > val (sss,ttt) = mk_set thy pt p consts pred;
117 > (Sign.string_of_term (sign_of thy) sss,Sign.string_of_term(sign_of thy) ttt);
118 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
120 val consts = str2term "UniversalList";
121 val pred = str2term "Assumptions";
127 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
128 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
129 val (consts,(bdv,pred)) = (ft,vp);
131 fun check_elementwise thy erls all_results (bdv, asm) =
132 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
134 let val inst_ = map (subst_atomic [sub]) asm
135 in case eval__true thy 1 inst_ [] erls of
136 (asm', true) => ([HOLogic.mk_eq sub], asm')
137 | (_, false) => ([],[])
139 (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^
140 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
141 val c' = isalist2list all_results
142 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
143 val subs = map (pair bdv) c''
144 in if asm = [] then (all_results, [])
145 else ((apfst ((list2isalist bool) o flat)) o
146 (apsnd flat) o split_list o (map check)) subs end;
148 > val all_results = str2term "[x=a+b,x=b,x=3]";
149 > val bdv = str2term "x";
150 > val asm = str2term "(x ~= a) & (x ~= b)";
152 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
153 > term2str t; writeln(terms2str ts);
154 val it = "[x = a + b, x = b, x = c]" : string
155 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
156 ... with appropriate erls this should be:
157 val it = "[x = a + b, x = c]" : string
158 ["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
159 ////// because b ~= b False*)
164 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
165 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
166 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
167 val ct' = "True" : cterm'
169 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
170 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
171 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
172 val ct' = "True" : cterm'
175 > val const = (term_of o the o (parse thy)) "(#3::real)";
176 > val pred' = subst_atomic [(bdv,const)] pred;
179 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
180 > val bdv = (term_of o the o (parse thy)) "(x::real)";
181 > val pred = (term_of o the o (parse thy))
182 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
183 > val ttt = check_elementwise thy consts (bdv, pred);
184 > cterm_of (sign_of thy) ttt;
185 val it = "[x = #-3, x = #3]" : cterm
187 > val consts = (term_of o the o (parse thy)) "[x = #4]";
188 > val bdv = (term_of o the o (parse thy)) "(x::real)";
189 > val pred = (term_of o the o (parse thy))
190 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
191 > val ttt = check_elementwise thy consts (bdv,pred);
192 > cterm_of (sign_of thy) ttt;
193 val it = "[x = #4]" : cterm
195 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
196 > val bdv = (term_of o the o (parse thy)) "(x::real)";
197 > val pred = (term_of o the o (parse thy))
198 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
199 > val ttt = check_elementwise thy consts (bdv,pred);
200 > cterm_of (sign_of thy) ttt;
201 val it = "[]" : cterm*)
204 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
205 fun split_dummy str =
206 let fun scan s' [] = (implode s', "")
207 | scan s' (s::ss) = if s=" " then (implode s', implode ss)
208 else scan (s'@[s]) ss;
209 in ((scan []) o explode) str end;
210 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
211 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
212 > split_dummy "x=-#5//#12";
213 val it = ("x=-#5//#12","") : string * string*)
218 (*.applicability of a tacic wrt. a calc-state (ptree,pos').
219 additionally used by next_tac in the script-interpreter for sequence-tacs.
220 tests for applicability are so expensive, that results (rewrites!)
221 are kept in the return-value of 'type tac_'.
223 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
224 Appl (Init_Proof' (ct', spec))
226 | applicable_in (p,p_) pt Model_Problem =
227 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
228 then Notappl ((tac2str Model_Problem)^
229 " not for pos "^(pos'2str (p,p_)))
230 else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
231 val {ppc,...} = get_pbt pI'
232 val pbl = init_pbl ppc
233 in Appl (Model_Problem' (pI', pbl, [])) end
234 (* val Refine_Tacitly pI = m;
236 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
237 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
238 then Notappl ((tac2str (Refine_Tacitly pI))^
239 " not for pos "^(pos'2str (p,p_)))
240 else (* val Refine_Tacitly pI = m;
242 let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
243 val opt = refine_ori oris pI;
246 Appl (Refine_Tacitly' (pI, pblID,
247 e_domID, e_metID, [](*filled in specify*)))
248 | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
249 " not applicable") end
251 val Refine_Problem pI = m;
253 | applicable_in (p,p_) pt (Refine_Problem pI) =
254 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
255 then Notappl ((tac2str (Refine_Problem pI))^
256 " not for pos "^(pos'2str (p,p_)))
258 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
259 probl=itms, ...}) = get_obj I pt p;
260 val thy = if dI' = e_domID then dI else dI';
261 val rfopt = refine_pbl (assoc_thy thy) pI itms;
263 NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
264 | SOME (rf as (pI',_)) =>
265 (* val SOME (rf as (pI',_)) = rfopt;
268 then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
269 else Appl (Refine_Problem' rf)
272 (*the specify-tacs have cterm' instead term:
273 parse+error here!!!: see appl_add*)
274 | applicable_in (p,p_) pt (Add_Given ct') =
275 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
276 then Notappl ((tac2str (Add_Given ct'))^
277 " not for pos "^(pos'2str (p,p_)))
278 else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
279 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
281 | applicable_in (p,p_) pt (Del_Given ct') =
282 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
283 then Notappl ((tac2str (Del_Given ct'))^
284 " not for pos "^(pos'2str (p,p_)))
285 else Appl (Del_Given' ct')
287 | applicable_in (p,p_) pt (Add_Find ct') =
288 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
289 then Notappl ((tac2str (Add_Find ct'))^
290 " not for pos "^(pos'2str (p,p_)))
291 else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
293 | applicable_in (p,p_) pt (Del_Find ct') =
294 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
295 then Notappl ((tac2str (Del_Find ct'))^
296 " not for pos "^(pos'2str (p,p_)))
297 else Appl (Del_Find' ct')
299 | applicable_in (p,p_) pt (Add_Relation ct') =
300 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
301 then Notappl ((tac2str (Add_Relation ct'))^
302 " not for pos "^(pos'2str (p,p_)))
303 else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
305 | applicable_in (p,p_) pt (Del_Relation ct') =
306 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
307 then Notappl ((tac2str (Del_Relation ct'))^
308 " not for pos "^(pos'2str (p,p_)))
309 else Appl (Del_Relation' ct')
311 | applicable_in (p,p_) pt (Specify_Theory dI) =
312 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
313 then Notappl ((tac2str (Specify_Theory dI))^
314 " not for pos "^(pos'2str (p,p_)))
315 else Appl (Specify_Theory' dI)
316 (* val (p,p_) = p; val Specify_Problem pID = m;
317 val Specify_Problem pID = m;
319 | applicable_in (p,p_) pt (Specify_Problem pID) =
320 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
321 then Notappl ((tac2str (Specify_Problem pID))^
322 " not for pos "^(pos'2str (p,p_)))
324 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
325 probl=itms, ...}) = get_obj I pt p;
326 val thy = assoc_thy (if dI' = e_domID then dI else dI');
327 val {ppc,where_,prls,...} = get_pbt pID;
328 val pbl = if pI'=e_pblID andalso pI=e_pblID
329 then (false, (init_pbl ppc, []))
330 else match_itms_oris thy itms (ppc,where_,prls) oris;
331 in Appl (Specify_Problem' (pID, pbl)) end
332 (* val Specify_Method mID = nxt; val (p,p_) = p;
334 | applicable_in (p,p_) pt (Specify_Method mID) =
335 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
336 then Notappl ((tac2str (Specify_Method mID))^
337 " not for pos "^(pos'2str (p,p_)))
338 else Appl (Specify_Method' (mID,[(*filled in specify*)],
339 [(*filled in specify*)]))
341 | applicable_in (p,p_) pt (Apply_Method mI) =
342 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
343 then Notappl ((tac2str (Apply_Method mI))^
344 " not for pos "^(pos'2str (p,p_)))
345 else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
347 | applicable_in (p,p_) pt (Check_Postcond pI) =
349 then Notappl ((tac2str (Check_Postcond pI))^
350 " not for pos "^(pos'2str (p,p_)))
351 else Appl (Check_Postcond'
352 (pI,(e_term,[(*asm in solve*)])))
353 (* in solve -"- ^^^^^^ gets returnvalue of scr*)
355 (*these are always applicable*)
356 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
357 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
359 (* val m as Rewrite_Inst (subs, thm') = m;
361 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
363 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
366 val pp = par_pblobj pt p;
367 val thy' = (get_obj g_domID pt pp):theory';
368 val thy = assoc_thy thy';
369 val {rew_ord'=ro',erls=erls,(*asm_thm=asm_thm,*)...} =
370 get_met (get_obj g_metID pt pp);
371 (*val put_asm = (fst thm') mem (map fst asm_thm);*)
372 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
373 Frm => (get_obj g_form pt p, p)
374 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
375 | _ => raise error ("applicable_in: call by "^
378 let val subst = subs2subst thy subs;
379 val subs' = subst2subs' subst;
380 in case rewrite_inst_ thy (assoc_rew_ord ro') erls
381 (*put_asm*)false subst (assoc_thm' thy thm') f of
382 SOME (f',asm) => Appl (
383 Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
384 (*term_of o the o (parse (assoc_thy thy'))*) f,
385 (*(term_of o the o (parse (assoc_thy thy'))*) (f',
386 (*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
387 | NONE => Notappl ((fst thm')^" not applicable") end
388 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
390 (* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
391 val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
393 | applicable_in (p,p_) pt (m as Rewrite thm') =
395 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
397 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
398 val thy = assoc_thy thy';
400 Frm => get_obj g_form pt p
401 | Res => (fst o (get_obj g_result pt)) p
402 | _ => raise error ("applicable_in Rewrite: call by "^
406 ((*writeln("### applicable_in rls'= "^rls');*)
407 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
409 case rewrite_ thy (assoc_rew_ord ro)
410 rls' false (assoc_thm' thy thm') f of
411 SOME (f',asm) => Appl (
412 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
413 | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
417 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
419 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
422 val pp = par_pblobj pt p;
423 val thy' = (get_obj g_domID pt pp):theory';
424 val thy = assoc_thy thy';
425 val {rew_ord'=ro',erls=erls,...} =
426 get_met (get_obj g_metID pt pp);
427 (*val put_asm = true;*)
428 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
429 Frm => (get_obj g_form pt p, p)
430 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
431 | _ => raise error ("applicable_in: call by "^
433 in case rewrite_ thy (assoc_rew_ord ro') erls
434 (*put_asm*)false (assoc_thm' thy thm') f of
435 SOME (f',asm) => Appl (
436 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
437 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
439 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
441 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
444 val pp = par_pblobj pt p;
445 val thy' = (get_obj g_domID pt pp):theory';
446 val thy = assoc_thy thy';
447 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
448 val f = case p_ of Frm => get_obj g_form pt p
449 | Res => (fst o (get_obj g_result pt)) p
450 | _ => raise error ("applicable_in: call by "^
453 let val subst = subs2subst thy subs
454 val subs' = subst2subs' subst
455 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
456 SOME (f',asm) => Appl (
457 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
458 | NONE => Notappl (rls^" not applicable") end
459 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
461 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
463 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
466 val pp = par_pblobj pt p;
467 val thy' = (get_obj g_domID pt pp):theory';
468 val thy = assoc_thy thy';
469 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
470 get_met (get_obj g_metID pt pp);
471 (*val put_asm = rls mem asm_rls;*)
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 | _ => raise 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) =
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 {asm_rls=asm_rls,...} = get_met (get_obj g_metID pt pp);
494 val put_asm = rls mem asm_rls;*)
495 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
496 Frm => (get_obj g_form pt p, p)
497 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
498 | _ => raise error ("applicable_in: call by "^
500 in case rewrite_set_ (assoc_thy thy') (*put_asm*)false (assoc_rls rls) f of
502 ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*)
503 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
505 | NONE => Notappl (rls^" not applicable") end
507 | applicable_in (p,p_) pt (m as Detail_Set rls) =
509 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
511 let val pp = par_pblobj pt p
512 val thy' = (get_obj g_domID pt pp):theory'
514 Frm => get_obj g_form pt p
515 | Res => (fst o (get_obj g_result pt)) p
516 | _ => raise error ("applicable_in: call by "^
518 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
520 Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
521 | NONE => Notappl (rls^" not applicable") end
524 | applicable_in p pt (End_Ruleset) =
525 raise error ("applicable_in: not impl. for "^
526 (tac2str End_Ruleset))
528 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
530 | applicable_in (p,p_) pt (m as Calculate op_) =
532 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
535 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
537 Frm => get_obj g_form pt p
538 | Res => (fst o (get_obj g_result pt)) p
539 in if msg = "OK" then
540 case calculate_ (assoc_thy thy') isa_fn f of
541 SOME (f', (id, thm)) =>
542 Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
543 | NONE => Notappl ("'calculate "^op_^"' not applicable")
547 (*Substitute combines two different kind of "substitution":
548 (1) subst_atomic: for ?a..?z
549 (2) Pattern.match: for solving equational systems
550 (which raises exn for ?a..?z)*)
551 | applicable_in (p,p_) pt (m as Substitute sube) =
553 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
554 else let val pp = par_pblobj pt p
555 val thy = assoc_thy (get_obj g_domID pt pp)
557 Frm => get_obj g_form pt p
558 | Res => (fst o (get_obj g_result pt)) p
559 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
560 val subte = sube2subte sube
561 val subst = sube2subst thy sube
562 in if foldl and_ (true, map contains_Var subte)
564 then let val f' = subst_atomic subst f
565 in if f = f' then Notappl (sube2str sube^" not applicable")
566 else Appl (Substitute' (subte, f, f'))
569 else case rewrite_terms_ thy (assoc_rew_ord rew_ord')
571 SOME (f', _) => Appl (Substitute' (subte, f, f'))
572 | NONE => Notappl (sube2str sube^" not applicable")
574 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
575 | applicable_in (p,p_) pt (m as Substitute sube) =
577 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
578 else let val pp = par_pblobj pt p
579 val thy = assoc_thy (get_obj g_domID pt pp)
581 Frm => get_obj g_form pt p
582 | Res => (fst o (get_obj g_result pt)) p
583 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
584 val subte = sube2subte sube
585 in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
586 SOME (f', _) => Appl (Substitute' (subte, f, f'))
587 | NONE => Notappl (sube2str sube^" not applicable")
591 | applicable_in p pt (Apply_Assumption cts') =
592 (raise error ("applicable_in: not impl. for "^
593 (tac2str (Apply_Assumption cts'))))
595 (*'logical' applicability wrt. script in locate: Inconsistent?*)
596 | applicable_in (p,p_) pt (m as Take ct') =
598 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
600 let val thy' = get_obj g_domID pt (par_pblobj pt p);
601 in (case parse (assoc_thy thy') ct' of
602 SOME ct => Appl (Take' (term_of ct))
603 | NONE => Notappl ("syntax error in "^ct'))
606 | applicable_in p pt (Take_Inst ct') =
607 raise error ("applicable_in: not impl. for "^
608 (tac2str (Take_Inst ct')))
610 | applicable_in p pt (Group (con, ints)) =
611 raise error ("applicable_in: not impl. for "^
612 (tac2str (Group (con, ints))))
614 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
616 then (*maybe Apply_Method has already been done*)
617 case get_obj g_env pt p of
618 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
619 e_term, [], subpbl domID pblID))
620 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
621 else (*somewhere later in the script*)
622 Appl (Subproblem' ((domID, pblID, e_metID), [],
623 e_term, [], subpbl domID pblID))
625 | applicable_in p pt (End_Subproblem) =
626 raise error ("applicable_in: not impl. for "^
627 (tac2str (End_Subproblem)))
629 | applicable_in p pt (CAScmd ct') =
630 raise error ("applicable_in: not impl. for "^
631 (tac2str (CAScmd ct')))
633 | applicable_in p pt (Split_And) =
634 raise error ("applicable_in: not impl. for "^
635 (tac2str (Split_And)))
636 | applicable_in p pt (Conclude_And) =
637 raise error ("applicable_in: not impl. for "^
638 (tac2str (Conclude_And)))
639 | applicable_in p pt (Split_Or) =
640 raise error ("applicable_in: not impl. for "^
641 (tac2str (Split_Or)))
642 | applicable_in p pt (Conclude_Or) =
643 raise error ("applicable_in: not impl. for "^
644 (tac2str (Conclude_Or)))
646 | applicable_in (p,p_) pt (Begin_Trans) =
648 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
649 (*_____ implizit Take in gen*)
650 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
651 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
652 | _ => raise error ("applicable_in: call by "^
654 val thy' = get_obj g_domID pt (par_pblobj pt p);
655 in (Appl (Begin_Trans' f))
656 handle _ => raise error ("applicable_in: Begin_Trans finds \
657 \syntaxerror in '"^(term2str f)^"'") end
659 (*TODO: check parent branches*)
660 | applicable_in (p,p_) pt (End_Trans) =
661 let val thy' = get_obj g_domID pt (par_pblobj pt p);
663 then Appl (End_Trans' (get_obj g_result pt p))
664 else Notappl "'End_Trans' is not applicable at \
665 \the beginning of a transitive sequence"
666 (*TODO: check parent branches*)
669 | applicable_in p pt (Begin_Sequ) =
670 raise error ("applicable_in: not impl. for "^
671 (tac2str (Begin_Sequ)))
672 | applicable_in p pt (End_Sequ) =
673 raise error ("applicable_in: not impl. for "^
674 (tac2str (End_Sequ)))
675 | applicable_in p pt (Split_Intersect) =
676 raise error ("applicable_in: not impl. for "^
677 (tac2str (Split_Intersect)))
678 | applicable_in p pt (End_Intersect) =
679 raise error ("applicable_in: not impl. for "^
680 (tac2str (End_Intersect)))
681 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
684 val Check_elementwise pred = m;
686 val ((p,p_), Check_elementwise pred) = (p, m);
688 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
690 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
693 val pp = par_pblobj pt p;
694 val thy' = (get_obj g_domID pt pp):theory';
695 val thy = assoc_thy thy'
696 val metID = (get_obj g_metID pt pp)
697 val {crls,...} = get_met metID
698 (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls)
699 val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*)
700 (*val erl = the (assoc'(!ruleset',crls))*)
701 val (f,asm) = case p_ of
702 Frm => (get_obj g_form pt p , [])
703 | Res => get_obj g_result pt p;
704 (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*)
705 val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
706 (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^
707 pair2str(term2str v,term2str p))*)
709 Const ("List.list.Cons",_) $ _ $ _ =>
710 Appl (Check_elementwise'
712 ((*writeln("### applicable_in Check_elementwise: --> "^
713 (res2str (check_elementwise thy crls f vp)));*)
714 check_elementwise thy crls f vp)))
715 | Const ("Tools.UniversalList",_) =>
716 Appl (Check_elementwise' (f, pred, (f,asm)))
717 | Const ("List.list.Nil",_) =>
718 (*Notappl "not applicable to empty list" 3.6.03*)
719 Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
720 | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
723 | applicable_in (p,p_) pt Or_to_List =
725 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
728 val pp = par_pblobj pt p;
729 val thy' = (get_obj g_domID pt pp):theory';
730 val thy = assoc_thy thy';
732 Frm => get_obj g_form pt p
733 | Res => (fst o (get_obj g_result pt)) p;
734 in (let val ls = or2list f
735 in Appl (Or_to_List' (f, ls)) end)
736 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
739 | applicable_in p pt (Collect_Trues) =
740 raise error ("applicable_in: not impl. for "^
741 (tac2str (Collect_Trues)))
743 | applicable_in p pt (Empty_Tac) =
744 Notappl "Empty_Tac is not applicable"
746 | applicable_in (p,p_) pt (Tac id) =
748 val pp = par_pblobj pt p;
749 val thy' = (get_obj g_domID pt pp):theory';
750 val thy = assoc_thy thy';
752 Frm => get_obj g_form pt p
753 | Res => (fst o (get_obj g_result pt)) p;
755 "subproblem_equation_dummy" =>
757 then Appl (Tac_ (thy, term2str f, id,
758 "subproblem_equation_dummy ("^(term2str f)^")"))
759 else Notappl "applicable only to equations made explicit"
760 | "solve_equation_dummy" =>
761 let (*val _= writeln("### applicable_in: solve_equation_dummy: f= "
763 val (id',f') = split_dummy (term2str f);
764 (*val _= writeln("### applicable_in: f'= "^f');*)
765 (*val _= (term_of o the o (parse thy)) f';*)
766 (*val _= writeln"### applicable_in: solve_equation_dummy";*)
767 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
768 else if is_expliceq ((term_of o the o (parse thy)) f')
769 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
770 else error ("applicable_in: f= " ^ f') end
771 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
773 | applicable_in p pt End_Proof' = Appl End_Proof''
775 | applicable_in _ _ m =
776 raise error ("applicable_in called for "^(tac2str m));
779 fun tac2tac_ pt p m =
780 case applicable_in p pt m of
782 | Notappl _ => raise error ("tac2mstp': fails with"^