Composing obtains-style lemma with OF

Viewed 36

I have obtains-style lemma (those that look like induction or case analysis lemmas), and I want to compose them:

notepad begin
  fix P Q Q1 Q2 R R'
  assume lemma1: "⋀ thesis. P ⟹ (Q ⟹ thesis) ⟹ (R ⟹ thesis) ⟹ thesis"
  assume lemma2: "⋀ thesis. Q ⟹ (Q1 ⟹ thesis) ⟹ (Q2 ⟹ thesis)  ⟹ thesis"
  assume lemma3: "⋀ thesis. R ⟹ (R' ⟹ thesis) ⟹ thesis"
  thm lemma1[OF _ lemma2 lemma3]
end

This shows

P ⟹
(Q ⟹ Q) ⟹ (Q ⟹ Q1 ⟹ ?thesis) ⟹ (Q ⟹ Q2 ⟹ ?thesis) ⟹
(R ⟹ R) ⟹ (R ⟹ R' ⟹ ?thesis) ⟹
?thesis

but I’d like to get

P ⟹
(Q1 ⟹ ?thesis) ⟹ (Q2 ⟹ ?thesis) ⟹
(R' ⟹ ?thesis) ⟹
?thesis

Is that possible without having to spell out the lemma?

0 Answers
Related