Focussing on new subgoals in Eisbach

In Eisbach I can use ; to apply a method to all new subgoals created by a method. However, I often know how many subgoals are created and would like to apply different methods to the new subgoals. Is there a way to say something like "apply method X to the first new subgoal and method Y to the second new subgoal"?

Here is a simple use case:

I want to develop a method that works on 2 conjunctions of arbitrary length but with the same structure. The method should be usable to show that conjunction 1 implies conjunction 2 by showing that the implication holds for each component. It should be usable like this:

lemma example:
  assumes c: "a 0 ∧ a 1 ∧ a 2  ∧ a 3"
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
proof (conj_one_by_one pre: c)
  show "a 0 ⟹ a' 0" by (rule imp)
  show "a 1 ⟹ a' 1" by (rule imp)
  show "a 2 ⟹ a' 2" by (rule imp)
  show "a 3 ⟹ a' 3" by (rule imp)
qed

When implementing this method in Eisbach, I have a problem after using rule conjI. I get two subgoals that I want to recursively work on, but I want to use different facts for the two cases.

I came up with the following workaround, which uses artificial markers for the two subgoals and is kind of ugly:

definition "marker_L x ≡ x"
definition "marker_R x ≡ x"

lemma conjI_marked: 
  assumes "marker_L P" and "marker_R Q"
  shows "P ∧ Q"
  using assms unfolding marker_L_def marker_R_def by simp


method conj_one_by_one uses pre = (
    match pre in 
      p: "?P ∧ ?Q" ⇒ ‹
        (unfold marker_L_def marker_R_def)?, 
        rule conjI_marked;( 
            (match conclusion in "marker_L _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct1])?›)
          | (match conclusion in "marker_R _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct2])?›))›)
    | ((unfold marker_L_def marker_R_def)?, insert pre)

Solution

This is not a complete answer, but you might be able to derive some useful information from what is stated here.

In Eisbach I can use ; to apply a method to all new subgoals created by a method. However, I often know how many subgoals are created and would like to apply different methods to the new subgoals. Is there a way to say something like "apply method X to the first new subgoal and method Y to the second new subgoal"?

You can use the standard tactical RANGE to define your own tactic that you can apply to consecutive subgoals. I provide a very specialized and significantly simplified use case below:

ML‹

fun mytac ctxt thms = thms
  |> map (fn thm => resolve_tac ctxt (single thm))
  |> RANGE

›

lemma 
  assumes A: A and B: B and C: C
  shows "A ∧ B ∧ C"
  apply(intro conjI)
  apply(tactic‹mytac @{context} [@{thm A}, @{thm B}, @{thm C}] 1›)
  done

Hopefully, it should be reasonably easy to extend it to more complicated use cases (while being more careful than I am about subgoal indexing: you might also need SELECT_GOAL to ensure that the implementation is safe). While in the example above mytac accepts a list of theorems, it should be easy to see how these theorems can be replaced by tactics and with some further work, the tactic can be wrapped as a higher-order method.

I want to develop a method that works on 2 conjunctions of arbitrary length but with the same structure. The method should be usable to show that conjunction 1 implies conjunction 2 by showing that the implication holds for each component. It should be usable like this:

UPDATE

Having had another look at the problem, it seems that there exists a substantially more natural solution. The solution follows the outline from the original answer, but the meta implication is replaced with the HOL's object logic implication (the 'to and fro' conversion can be achieved using atomize (full) and intro impI):

lemma arg_imp2: "(a ⟶ b) ⟹ (c ⟶ d) ⟹ ((a ∧ c) ⟶ (b ∧ d))" by auto

lemma example:
  assumes "a 0 ∧ a 1 ∧ a 2 ∧ a 3" 
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
  apply(insert assms(1), atomize (full))
  apply(intro arg_imp2; intro impI; intro imp; assumption)
  done

LEGACY (this was part of the original answer, but is almost irrelevant due to the UPDATE suggested above)

If this is the only application that you have in mind, perhaps, there is a reasonably natural solution based on the following iterative procedure:

lemma arg_imp2: "(a ⟹ b) ⟹ (c ⟹ d) ⟹ ((a ∧ c) ⟹ (b ∧ d))" by auto

lemma example:
  assumes c: "a 0 ∧ a 1 ∧ a 2 ∧ a 3"
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
  using c
  apply(intro arg_imp2[of ‹a 0› ‹a' 0› ‹a 1 ∧ a 2 ∧ a 3› ‹a' 1 ∧ a' 2 ∧ a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(intro arg_imp2[of ‹a 1› ‹a' 1› ‹a 2 ∧ a 3› ‹a' 2 ∧ a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(intro arg_imp2[of ‹a 2› ‹a' 2› ‹a 3› ‹a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(rule imp)
  apply(assumption+)
  done

I am not certain how easy it would be to express this in Eisbach, but it should be reasonably easy to express this in Isabelle/ML.