259 Frm => (get_obj g_form pt p, p) |
259 Frm => (get_obj g_form pt p, p) |
260 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
260 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
261 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
261 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
262 in |
262 in |
263 let |
263 let |
264 val subst = Selem.subs2subst thy subs; |
264 val subst = Subst.T_from_input thy subs; |
265 in |
265 in |
266 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of |
266 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of |
267 SOME (f',asm) => |
267 SOME (f',asm) => |
268 Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) |
268 Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) |
269 | NONE => Notappl ((fst thm'')^" not applicable") |
269 | NONE => Notappl ((fst thm'')^" not applicable") |
298 val thy' = get_obj g_domID pt pp; |
298 val thy' = get_obj g_domID pt pp; |
299 val thy = ThyC.get_theory thy'; |
299 val thy = ThyC.get_theory thy'; |
300 val f = case p_ of Frm => get_obj g_form pt p |
300 val f = case p_ of Frm => get_obj g_form pt p |
301 | Res => (fst o (get_obj g_result pt)) p |
301 | Res => (fst o (get_obj g_result pt)) p |
302 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
302 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
303 val subst = Selem.subs2subst thy subs |
303 val subst = Subst.T_from_input thy subs |
304 in |
304 in |
305 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of |
305 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of |
306 SOME (f', asm) |
306 SOME (f', asm) |
307 => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
307 => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
308 | NONE => Notappl (rls ^ " not applicable") |
308 | NONE => Notappl (rls ^ " not applicable") |
318 val thy = ThyC.get_theory thy'; |
318 val thy = ThyC.get_theory thy'; |
319 val (f, _) = case p_ of |
319 val (f, _) = case p_ of |
320 Frm => (get_obj g_form pt p, p) |
320 Frm => (get_obj g_form pt p, p) |
321 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
321 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
322 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
322 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
323 val subst = Selem.subs2subst thy subs; |
323 val subst = Subst.T_from_input thy subs; |
324 in |
324 in |
325 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of |
325 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of |
326 SOME (f',asm) |
326 SOME (f',asm) |
327 => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
327 => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
328 | NONE => Notappl (rls ^ " not applicable") |
328 | NONE => Notappl (rls ^ " not applicable") |
394 val f = case p_ of |
394 val f = case p_ of |
395 Frm => get_obj g_form pt p |
395 Frm => get_obj g_form pt p |
396 | Res => (fst o (get_obj g_result pt)) p |
396 | Res => (fst o (get_obj g_result pt)) p |
397 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
397 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
398 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp) |
398 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp) |
399 val subte = Selem.sube2subte sube |
399 val subte = Subst.tyty_to_eqs sube |
400 val subst = Selem.sube2subst thy sube |
400 val subst = Subst.T_from_tyty thy sube |
401 val ro = Rewrite_Ord.assoc_rew_ord rew_ord' |
401 val ro = Rewrite_Ord.assoc_rew_ord rew_ord' |
402 in |
402 in |
403 if foldl and_ (true, map TermC.contains_Var subte) |
403 if foldl and_ (true, map TermC.contains_Var subte) |
404 then (*1*) |
404 then (*1*) |
405 let val f' = subst_atomic subst f |
405 let val f' = subst_atomic subst f |
406 in if f = f' |
406 in if f = f' |
407 then Notappl (Selem.sube2str sube^" not applicable") |
407 then Notappl (Subst.tyty_to_string sube^" not applicable") |
408 else Appl (Tactic.Substitute' (ro, erls, subte, f, f')) |
408 else Appl (Tactic.Substitute' (ro, erls, subte, f, f')) |
409 end |
409 end |
410 else (*2*) |
410 else (*2*) |
411 case Rewrite.rewrite_terms_ thy ro erls subte f of |
411 case Rewrite.rewrite_terms_ thy ro erls subte f of |
412 SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f')) |
412 SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f')) |
413 | NONE => Notappl (Selem.sube2str sube ^ " not applicable") |
413 | NONE => Notappl (Subst.tyty_to_string sube ^ " not applicable") |
414 end |
414 end |
415 | applicable_in _ _ (Tactic.Apply_Assumption cts') = |
415 | applicable_in _ _ (Tactic.Apply_Assumption cts') = |
416 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts')) |
416 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts')) |
417 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *) |
417 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *) |
418 | applicable_in _ _ (Tactic.Take_Inst ct') = |
418 | applicable_in _ _ (Tactic.Take_Inst ct') = |