Initial proof method to consume all incoming facts

Question

Assume I have a goal A ⟹ B ⟹ C ⟹ G The goal is unwieldy (generated from some proof obligation), and it appears (in similar shape) several times in my development.

So I create a lemma foo to simplify the goal, of the shape A ⟹ C ⟹ (P ⟹ Q) ⟹ G.

I’d like to be able to write

case goal42
  thus ?case
  proof (rule foo)
    assume P
    show Q sorry
  qed

but this fails, because foo does not use B. What works is

case goal42
  thus ?case
    apply -
    apply (erule (1) eqvt_lam_case)
    proof-
    assume P
    show Q sorry
  qed

but this style of opening a proof in the middle of an apply script is considered bad practice.

Is there a method similar to rule that is a bit smarter in matching the incoming facts against the hypothesis of the rule? Ideally it reads a consumes 2 parameter on foo to figure out how many hypothesis should match.

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2014-07-09T09:56:45

The method rule is very picky about which facts are chained in. Its precursors intro and elim do not complain if chained-in facts do not fit; intro does not match against them at all. elim ... roughly corresponds to apply - apply(erule ...)+, so this might approximate what you are looking for. But I do not know of a way to tell elim to match multiple assumptions, and there elim tries to apply the given rules as long as possible, which might not be what you want.

However, since you open an Isar proof for the remaining goal anyway, you can rearrange your proof and avoid the issue.

case goal42
{ assume P
  show Q sorry }
with goal42 show ?case by-(erule (2) eqvt_lam_case)

Initial proof method to consume all incoming facts

1 Answers