CODEWITHSUNDEEP
isabelle
Joachim Breitner
Joachim Breitner

Reputation: 25763

Initial proof method to consume all incoming facts

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.

Upvotes: 0

Views: 78

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

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)

Upvotes: 2

Related Questions