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\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk> \<Longrightarrow> C" apply (rprems 2) -- "Explicitely specify number of premise" apply (rprems 1) . lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; 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