[isabelle-dev] Resolve with premises

[Peter Lammich]

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)
  .

--------------------------