Hi all,
as the question currently arose on the users list, I remembered that I
have the following method laying around since several month. I'm using
it frequently in apply-style scripts (Mainly to apply induction
hypotheses).
We discussed here in Munich whether we should add it to Isabelle. Should
we? Opinions?
Peter
---
ML {*
(* Resolve with premises. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprems_tac ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i)
=
let
fun non_atomic (Const (==, _) $ _ $ _) = true
| non_atomic (Const (all, _) $ _) = true
| non_atomic _ = false;
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of)
(Drule.strip_imp_prems goal'');
val ethms = Rs | map (fn R =
(Raw_Simplifier.norm_hhf (Thm.trivial R)));
in eresolve_tac ethms i end
);
(* Resolve with premise. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprem_tac n ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal,
i) =
let
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val R = nth (Drule.strip_imp_prems goal'') (n - 1)
val rl = Raw_Simplifier.norm_hhf (Thm.trivial R)
in
etac rl i
end
);
val setup =
Method.setup @{binding rprems}
(Scan.lift (Scan.option Parse.nat) (fn i = fn ctxt =
SIMPLE_METHOD' (
case i of
NONE = rprems_tac ctxt
| SOME i = rprem_tac i ctxt
))
)
Resolve with premises
*}
setup setup
(* EXAMPLES: *)
lemma \lbrakk A\LongrightarrowB; B\LongrightarrowC; A \rbrakk
\Longrightarrow C
apply (rprems 2) -- Explicitely specify number of premise
apply (rprems 1)
.
lemma \lbrakk A\LongrightarrowB; B\LongrightarrowC; A \rbrakk
\Longrightarrow C
apply (rprems) -- Resolve with any matching premise,
first to last, backtracking
apply (rprems)
.
--
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
