372 | _ => error ("applicable_in: call by " ^ pos'2str (p,p_)); |
372 | _ => error ("applicable_in: call by " ^ pos'2str (p,p_)); |
373 in |
373 in |
374 let |
374 let |
375 val subst = subs2subst thy subs; |
375 val subst = subs2subst thy subs; |
376 val subs' = subst2subs' subst; |
376 val subs' = subst2subs' subst; |
377 in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm' thy thm') f of |
377 val thm = assoc_thm'' thy thm'' |
|
378 in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst thm f of |
378 SOME (f',asm) => |
379 SOME (f',asm) => |
379 Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm', f, (f', asm))) |
380 Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) |
380 | NONE => Notappl ((fst thm')^" not applicable") |
381 | NONE => Notappl (fst thm'' ^ " not applicable") |
381 end |
382 end |
382 handle _ => Notappl ("syntax error in "^(subs2str subs)) |
383 handle _ => Notappl ("syntax error in "^(subs2str subs)) |
383 end |
384 end |
384 |
385 |
385 | applicable_in (p,p_) pt (m as Rewrite thm') = |
386 | applicable_in (p,p_) pt (m as Rewrite thm'') = |
386 if member op = [Pbl,Met] p_ |
387 if member op = [Pbl,Met] p_ |
387 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
388 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
388 else |
389 else |
389 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt; |
390 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm'' p pt; |
390 val thy = assoc_thy thy'; |
391 val thy = assoc_thy thy'; |
391 val f = case p_ of |
392 val f = case p_ of |
392 Frm => get_obj g_form pt p |
393 Frm => get_obj g_form pt p |
393 | Res => (fst o (get_obj g_result pt)) p |
394 | Res => (fst o (get_obj g_result pt)) p |
394 | _ => error ("applicable_in Rewrite: call by "^ |
395 | _ => error ("applicable_in Rewrite: call by "^ |
395 (pos'2str (p,p_))); |
396 (pos'2str (p,p_))); |
396 in if msg = "OK" |
397 in if msg = "OK" |
397 then |
398 then |
398 ((*tracing("### applicable_in rls'= "^rls');*) |
399 ((*tracing("### applicable_in rls'= "^rls');*) |
399 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f; |
400 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f; |
400 *) |
401 *) |
401 case rewrite_ thy (assoc_rew_ord ro) |
402 let val thm = assoc_thm'' thy thm'' |
402 rls' false (assoc_thm' thy thm') f of |
403 in case rewrite_ thy (assoc_rew_ord ro) rls' false thm f of |
403 SOME (f',asm) => Appl ( |
404 SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) |
404 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm))) |
405 | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") |
405 | NONE => Notappl ("'"^(fst thm')^"' not applicable") ) |
406 end) |
406 else Notappl msg |
407 else Notappl msg |
407 end |
408 end |
408 |
409 |
409 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') = |
410 | applicable_in (p,p_) pt (m as Rewrite_Asm thm'') = |
410 if member op = [Pbl,Met] p_ |
411 if member op = [Pbl,Met] p_ |
411 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
412 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
412 else |
413 else |
413 let |
414 let |
414 val pp = par_pblobj pt p; |
415 val pp = par_pblobj pt p; |
415 val thy' = (get_obj g_domID pt pp):theory'; |
416 val thy' = (get_obj g_domID pt pp):theory'; |
416 val thy = assoc_thy thy'; |
417 val thy = assoc_thy thy'; |
417 val {rew_ord'=ro',erls=erls,...} = |
418 val {rew_ord'=ro',erls=erls,...} = |
418 get_met (get_obj g_metID pt pp); |
419 get_met (get_obj g_metID pt pp); |
419 (*val put_asm = true;*) |
420 (*val put_asm = true;*) |
420 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
421 val (f, _) = case p_ of |
421 Frm => (get_obj g_form pt p, p) |
422 Frm => (get_obj g_form pt p, p) |
422 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
423 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
423 | _ => error ("applicable_in: call by "^ |
424 | _ => error ("applicable_in: call by "^ |
424 (pos'2str (p,p_))); |
425 (pos'2str (p,p_))); |
425 in case rewrite_ thy (assoc_rew_ord ro') erls |
426 val thm = assoc_thm'' thy thm'' |
426 (*put_asm*)false (assoc_thm' thy thm') f of |
427 in case rewrite_ thy (assoc_rew_ord ro') erls false thm f of |
427 SOME (f',asm) => Appl ( |
428 SOME (f',asm) => Appl ( |
428 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm))) |
429 Rewrite' (thy', ro', erls, false, thm, f, (f', asm))) |
429 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end |
430 | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end |
430 |
431 |
431 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = |
432 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = |
432 if member op = [Pbl,Met] p_ |
433 if member op = [Pbl,Met] p_ |
433 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
434 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
434 else |
435 else |